Theorem 0zd 10888

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 10887	. 2 |- 0 e. ZZ
2	1	a1i 11	1 |- ( ph -> 0 e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1767   0cc0 9504   ZZcz 10876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-i2m1 9572  ax-1ne0 9573  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-iota 5557  df-fv 5602  df-ov 6298  df-neg 9820  df-z 10877

This theorem is referenced by:  fzctr  11796  fzosubel3  11857  bcval5  12376  ccatsymb  12580  ccat2s1fvw  12622  swrdspsleq  12653  swrdccatin12lem2b  12691  swrdccat  12698  repswswrd  12736  fzomaxdiflem  13155  fsumzcl  13537  isumnn0nn  13634  climcndslem1  13641  climcnds  13643  harmonic  13650  geolim  13659  geolim2  13660  geoisum  13666  geoisumr  13667  mertenslem1  13673  mertenslem2  13674  mertens  13675  eff  13696  efcvg  13699  reefcl  13701  efcj  13706  eftlub  13722  effsumlt  13724  eflegeo  13734  eirrlem  13815  ruclem6  13846  dvdsmod  13919  bitsinv1lem  13967  sadcf  13979  sadadd3  13987  smupf  14004  alginv  14080  algcvg  14081  algcvga  14084  algfx  14085  eucalgcvga  14091  eucalg  14092  phiprmpw  14182  fermltl  14190  iserodd  14235  pcpre1  14242  qexpz  14296  prmreclem4  14313  vdwapun  14368  odf1  16457  srgbinomlem4  17066  evlslem1  18054  cpmadugsumlemF  19246  dvnff  22194  dgrcl  22498  dgrub  22499  dgrlb  22501  elqaalem2  22583  elqaalem3  22584  geolim3  22602  tayl0  22624  dvtaylp  22632  radcnvlem1  22675  radcnvlem3  22677  radcnv0  22678  radcnvlt2  22681  pserulm  22684  psercn2  22685  pserdvlem2  22690  pserdv2  22692  abelthlem4  22696  abelthlem5  22697  abelthlem6  22698  abelthlem7  22700  abelthlem8  22701  abelthlem9  22702  cosne0  22783  logtayl  22907  leibpi  23139  leibpisum  23140  log2cnv  23141  log2tlbnd  23142  basellem3  23222  dchrptlem2  23406  bcmono  23418  lgslem4  23440  lgsne0  23474  numclwwlkovf2ex  24901  archiabllem1b  27551  oddpwdc  28109  ballotlemfval0  28250  risefacval2  29050  fallfacval2  29051  binomfallfaclem2  29080  bpolydiflem  29734  itg2addnclem2  29985  rmynn  30813  jm2.24nn  30816  jm2.17c  30819  jm2.24  30820  acongrep  30837  acongeq  30840  dvdsabsmod0  30847  jm2.18  30849  jm2.23  30857  jm2.20nn  30858  jm2.27a  30866  jm2.27c  30868  rmydioph  30875  hashnzfz  31140  stoweidlem11  31625  stoweidlem26  31640  stoweidlem34  31648  stirlinglem5  31692  fourierdlem12  31733  fourierdlem41  31762  fourierdlem48  31769  2ffzoeq  32122  0even  32306  2zrngamgm  32312  altgsumbcALT  32376