Theorem 0zd 10772

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

Syntax hints:   -> wi 4   e. wcel 1758   0cc0 9396   ZZcz 10760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-addrcl 9457  ax-mulcl 9458  ax-mulrcl 9459  ax-i2m1 9464  ax-1ne0 9465  ax-rnegex 9467  ax-rrecex 9468  ax-cnre 9469

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-iota 5492  df-fv 5537  df-ov 6206  df-neg 9712  df-z 10761

This theorem is referenced by:  fzctr  11649  fzosubel3  11721  bcval5  12214  ccatsymb  12402  swrdspsleq  12463  swrdccatin12lem2b  12498  swrdccat  12505  repswswrd  12543  fzomaxdiflem  12951  fsumzcl  13333  isumnn0nn  13426  climcndslem1  13433  climcnds  13435  harmonic  13442  geolim  13451  geolim2  13452  geoisum  13458  geoisumr  13459  mertenslem1  13465  mertenslem2  13466  mertens  13467  eff  13488  efcvg  13491  reefcl  13493  efcj  13498  eftlub  13514  effsumlt  13516  eflegeo  13526  eirrlem  13607  ruclem6  13638  dvdsmod  13711  bitsinv1lem  13758  sadcf  13770  sadadd3  13778  smupf  13795  alginv  13871  algcvg  13872  algcvga  13875  algfx  13876  eucalgcvga  13882  eucalg  13883  phiprmpw  13972  fermltl  13980  iserodd  14023  pcpre1  14030  qexpz  14084  prmreclem4  14101  vdwapun  14156  odf1  16187  srgbinomlem4  16767  evlslem1  17728  dvnff  21533  dgrcl  21837  dgrub  21838  dgrlb  21840  elqaalem2  21922  elqaalem3  21923  geolim3  21941  tayl0  21963  dvtaylp  21971  radcnvlem1  22014  radcnvlem3  22016  radcnv0  22017  radcnvlt2  22020  pserulm  22023  psercn2  22024  pserdvlem2  22029  pserdv2  22031  abelthlem4  22035  abelthlem5  22036  abelthlem6  22037  abelthlem7  22039  abelthlem8  22040  abelthlem9  22041  cosne0  22122  logtayl  22241  leibpi  22473  leibpisum  22474  log2cnv  22475  log2tlbnd  22476  basellem3  22556  dchrptlem2  22740  bcmono  22752  lgslem4  22774  lgsne0  22808  archiabllem1b  26374  oddpwdc  26901  ballotlemfval0  27042  risefacval2  27677  fallfacval2  27678  binomfallfaclem2  27707  bpolydiflem  28361  itg2addnclem2  28612  rmynn  29467  jm2.24nn  29470  jm2.17c  29473  jm2.24  29474  acongrep  29491  acongeq  29494  dvdsabsmod0  29503  jm2.18  29505  jm2.23  29513  jm2.20nn  29514  jm2.27a  29522  jm2.27c  29524  rmydioph  29531  stoweidlem11  29974  stoweidlem26  29989  stoweidlem34  29997  stirlinglem5  30041  2ffzoeq  30382  numclwwlkovf2ex  30847  altgsumbcALT  30918  cpmadugsumlemF  31382