Theorem 0zd 10650

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

Syntax hints:   -> wi 4   e. wcel 1756   0cc0 9274   ZZcz 10638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-neg 9590  df-z 10639

This theorem is referenced by:  fzctr  11521  fzosubel3  11593  bcval5  12086  ccatsymb  12273  swrdspsleq  12334  swrdccatin12lem2b  12369  swrdccat  12376  repswswrd  12414  fzomaxdiflem  12822  fsumzcl  13204  isumnn0nn  13297  climcndslem1  13304  climcnds  13306  harmonic  13313  geolim  13322  geolim2  13323  geoisum  13329  geoisumr  13330  mertenslem1  13336  mertenslem2  13337  mertens  13338  eff  13359  efcvg  13362  reefcl  13364  efcj  13369  eftlub  13385  effsumlt  13387  eflegeo  13397  eirrlem  13478  ruclem6  13509  dvdsmod  13582  bitsinv1lem  13629  sadcf  13641  sadadd3  13649  smupf  13666  alginv  13742  algcvg  13743  algcvga  13746  algfx  13747  eucalgcvga  13753  eucalg  13754  phiprmpw  13843  fermltl  13851  iserodd  13894  pcpre1  13901  qexpz  13955  prmreclem4  13972  vdwapun  14027  odf1  16054  srgbinomlem4  16629  evlslem1  17576  dvnff  21372  dgrcl  21676  dgrub  21677  dgrlb  21679  elqaalem2  21761  elqaalem3  21762  geolim3  21780  tayl0  21802  dvtaylp  21810  radcnvlem1  21853  radcnvlem3  21855  radcnv0  21856  radcnvlt2  21859  pserulm  21862  psercn2  21863  pserdvlem2  21868  pserdv2  21870  abelthlem4  21874  abelthlem5  21875  abelthlem6  21876  abelthlem7  21878  abelthlem8  21879  abelthlem9  21880  cosne0  21961  logtayl  22080  leibpi  22312  leibpisum  22313  log2cnv  22314  log2tlbnd  22315  basellem3  22395  dchrptlem2  22579  bcmono  22591  lgslem4  22613  lgsne0  22647  archiabllem1b  26160  oddpwdc  26689  ballotlemfval0  26830  risefacval2  27464  fallfacval2  27465  binomfallfaclem2  27494  bpolydiflem  28148  itg2addnclem2  28397  rmynn  29252  jm2.24nn  29255  jm2.17c  29258  jm2.24  29259  acongrep  29276  acongeq  29279  dvdsabsmod0  29288  jm2.18  29290  jm2.23  29298  jm2.20nn  29299  jm2.27a  29307  jm2.27c  29309  rmydioph  29316  stoweidlem11  29759  stoweidlem26  29774  stoweidlem34  29782  stirlinglem5  29826  2ffzoeq  30167  numclwwlkovf2ex  30632  altgsumbcALT  30701