Theorem 0zd 10872

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

Syntax hints:   -> wi 4   e. wcel 1823   0cc0 9481   ZZcz 10860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-neg 9799  df-z 10861

This theorem is referenced by:  fzctr  11791  fzosubel3  11858  bcval5  12378  wrdsymb0  12563  ccatsymb  12589  swrdspsleq  12665  swrdccatin12lem2b  12702  swrdccat  12709  repswswrd  12747  fzomaxdiflem  13257  fsumzcl  13639  isumnn0nn  13736  climcndslem1  13743  climcnds  13745  harmonic  13752  geolim  13761  geolim2  13762  geoisum  13768  geoisumr  13769  mertenslem1  13775  mertenslem2  13776  mertens  13777  eff  13899  efcvg  13902  reefcl  13904  efcj  13909  eftlub  13926  effsumlt  13928  eflegeo  13938  eirrlem  14019  ruclem6  14052  dvdsmod  14127  bitsinv1lem  14175  sadcf  14187  sadadd3  14195  smupf  14212  alginv  14288  algcvg  14289  algcvga  14292  algfx  14293  eucalgcvga  14299  eucalg  14300  phiprmpw  14390  fermltl  14398  iserodd  14443  pcpre1  14450  qexpz  14504  prmreclem4  14521  vdwapun  14576  odf1  16783  srgbinomlem4  17389  evlslem1  18379  cpmadugsumlemF  19544  dvnff  22492  dgrcl  22796  dgrub  22797  dgrlb  22799  elqaalem2  22882  elqaalem3  22883  geolim3  22901  tayl0  22923  dvtaylp  22931  radcnvlem1  22974  radcnvlem3  22976  radcnv0  22977  radcnvlt2  22980  pserulm  22983  psercn2  22984  pserdvlem2  22989  pserdv2  22991  abelthlem4  22995  abelthlem5  22996  abelthlem6  22997  abelthlem7  22999  abelthlem8  23000  abelthlem9  23001  cosne0  23083  logtayl  23209  leibpi  23470  leibpisum  23471  log2cnv  23472  log2tlbnd  23473  basellem3  23554  dchrptlem2  23738  bcmono  23750  lgslem4  23772  lgsne0  23806  numclwwlkovf2ex  25288  archiabllem1b  27970  oddpwdc  28557  ballotlemfval0  28698  risefacval2  29373  fallfacval2  29374  binomfallfaclem2  29403  bpolydiflem  30044  itg2addnclem2  30307  rmynn  31133  jm2.24nn  31136  jm2.17c  31139  jm2.24  31140  acongrep  31157  acongeq  31160  dvdsabsmod0  31167  jm2.18  31169  jm2.23  31177  jm2.20nn  31178  jm2.27a  31186  jm2.27c  31188  rmydioph  31195  hashnzfz  31466  bccbc  31491  binomcxplemnn0  31495  binomcxplemrat  31496  binomcxplemnotnn0  31502  mccllem  31844  expfac  31902  sinaover2ne0  31907  dvnmul  31979  dvnprodlem1  31982  dvnprodlem2  31983  stoweidlem11  32032  stoweidlem26  32047  stoweidlem34  32055  stirlinglem5  32099  fourierdlem11  32139  fourierdlem12  32140  fourierdlem14  32142  fourierdlem15  32143  fourierdlem24  32152  fourierdlem25  32153  fourierdlem36  32164  fourierdlem37  32165  fourierdlem41  32169  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem64  32192  fourierdlem69  32197  fourierdlem73  32201  fourierdlem79  32207  fourierdlem81  32209  fourierdlem92  32220  fourierdlem93  32221  fourierdlem111  32239  elaa2lem  32255  etransclem3  32259  etransclem7  32263  etransclem10  32266  etransclem24  32280  etransclem27  32283  etransclem35  32291  etransclem44  32300  etransclem46  32302  etransclem47  32303  etransclem48  32304  pfxnd  32623  pfxccatin12lem1  32651  2ffzoeq  32715  0even  32991  2zrngamgm  32999  altgsumbcALT  33196  expnegico01  33377  dig0  33481  nn0sumshdiglem2  33497