Theorem 0zd 9267

Description: Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0zd	⊢ (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 9266	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2148  0cc0 7813  ℤcz 9255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7907  ax-addrcl 7910  ax-rnegex 7922

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880  df-neg 8133  df-z 9256

This theorem is referenced by:  fzctr  10135  fzosubel3  10198  frecfzennn  10428  frechashgf1o  10430  0tonninf  10441  1tonninf  10442  exp3val  10524  exp0  10526  bcval  10731  bccmpl  10736  bcval5  10745  bcpasc  10748  bccl  10749  hashcl  10763  hashfiv01gt1  10764  hashfz1  10765  hashen  10766  fihashneq0  10776  omgadd  10784  fihashdom  10785  fiubz  10811  fnfz0hash  10814  ffzo0hash  10816  fzomaxdiflem  11123  fsumzcl  11412  fisum0diag  11451  fisum0diag2  11457  binomlem  11493  binom1dif  11497  isumnn0nn  11503  expcnvre  11513  explecnv  11515  pwm1geoserap1  11518  geolim  11521  geolim2  11522  geo2sum  11524  geoisum  11527  geoisumr  11528  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  fprod0diagfz  11638  eftcl  11664  efval  11671  eff  11673  efcvg  11676  efcvgfsum  11677  reefcl  11678  ege2le3  11681  efcj  11683  efaddlem  11684  eftlub  11700  effsumlt  11702  efgt1p2  11705  efgt1p  11706  eflegeo  11711  eirraplem  11786  dvdsmodexp  11804  dvdsmod  11870  gcdn0gt0  11981  gcdaddm  11987  gcdmultipled  11996  bezoutlemle  12011  nn0seqcvgd  12043  alginv  12049  algcvg  12050  algcvga  12053  algfx  12054  eucalgval2  12055  eucalgcvga  12060  eucalg  12061  lcmcllem  12069  lcmid  12082  mulgcddvds  12096  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  phiprmpw  12224  modprm0  12256  pcpremul  12295  pceu  12297  pcmul  12303  pcqmul  12305  pcge0  12314  pcdvdsb  12321  pcneg  12326  pcgcd1  12329  pc2dvds  12331  pcz  12333  dvdsprmpweqle  12338  qexpz  12352  ennnfonelemjn  12405  ennnfonelemh  12407  ennnfonelem0  12408  ennnfonelem1  12410  ennnfonelemom  12411  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemex  12417  ennnfonelemrn  12422  ennnfonelemnn0  12425  ctinfomlemom  12430  mulgval  12991  mulgfng  12992  subgmulg  13053  lgsval  14490  lgsfvalg  14491  lgscllem  14493  lgsval2lem  14496  lgsneg1  14511  lgsne0  14524  012of  14830  2o01f  14831  isomninnlem  14863  iswomninnlem  14882  ismkvnnlem  14885  dceqnconst  14893  dcapnconst  14894