Theorem 0zd 9265

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

Assertion

Ref	Expression
0zd	|- ( ph -> 0 e. ZZ )

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 9264	. 2 |- 0 e. ZZ
2	1	a1i 9	1 |- ( ph -> 0 e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2148   0cc0 7811   ZZcz 9253

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 7905  ax-addrcl 7908  ax-rnegex 7920

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878  df-neg 8131  df-z 9254

This theorem is referenced by:  fzctr  10133  fzosubel3  10196  frecfzennn  10426  frechashgf1o  10428  0tonninf  10439  1tonninf  10440  exp3val  10522  exp0  10524  bcval  10729  bccmpl  10734  bcval5  10743  bcpasc  10746  bccl  10747  hashcl  10761  hashfiv01gt1  10762  hashfz1  10763  hashen  10764  fihashneq0  10774  omgadd  10782  fihashdom  10783  fiubz  10809  fnfz0hash  10812  ffzo0hash  10814  fzomaxdiflem  11121  fsumzcl  11410  fisum0diag  11449  fisum0diag2  11455  binomlem  11491  binom1dif  11495  isumnn0nn  11501  expcnvre  11511  explecnv  11513  pwm1geoserap1  11516  geolim  11519  geolim2  11520  geo2sum  11522  geoisum  11525  geoisumr  11526  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  fprod0diagfz  11636  eftcl  11662  efval  11669  eff  11671  efcvg  11674  efcvgfsum  11675  reefcl  11676  ege2le3  11679  efcj  11681  efaddlem  11682  eftlub  11698  effsumlt  11700  efgt1p2  11703  efgt1p  11704  eflegeo  11709  eirraplem  11784  dvdsmodexp  11802  dvdsmod  11868  gcdn0gt0  11979  gcdaddm  11985  gcdmultipled  11994  bezoutlemle  12009  nn0seqcvgd  12041  alginv  12047  algcvg  12048  algcvga  12051  algfx  12052  eucalgval2  12053  eucalgcvga  12058  eucalg  12059  lcmcllem  12067  lcmid  12080  mulgcddvds  12094  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  phiprmpw  12222  modprm0  12254  pcpremul  12293  pceu  12295  pcmul  12301  pcqmul  12303  pcge0  12312  pcdvdsb  12319  pcneg  12324  pcgcd1  12327  pc2dvds  12329  pcz  12331  dvdsprmpweqle  12336  qexpz  12350  ennnfonelemjn  12403  ennnfonelemh  12405  ennnfonelem0  12406  ennnfonelem1  12408  ennnfonelemom  12409  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemrn  12420  ennnfonelemnn0  12423  ctinfomlemom  12428  mulgval  12986  mulgfng  12987  subgmulg  13048  lgsval  14408  lgsfvalg  14409  lgscllem  14411  lgsval2lem  14414  lgsneg1  14429  lgsne0  14442  012of  14748  2o01f  14749  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803  dceqnconst  14810  dcapnconst  14811