Theorem 0zd 10900

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

Syntax hints:   -> wi 4   e. wcel 1872   0cc0 9490   ZZcz 10888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-iota 5508  df-fv 5552  df-ov 6252  df-neg 9814  df-z 10889

This theorem is referenced by:  fzctr  11854  fzosubel3  11925  bcval5  12453  wrdsymb0  12649  ccatsymb  12675  swrdspsleq  12751  swrdccatin12lem2b  12788  swrdccat  12795  repswswrd  12833  fzomaxdiflem  13349  fsumzcl  13744  isumnn0nn  13843  climcndslem1  13850  climcnds  13852  harmonic  13860  geolim  13869  geolim2  13870  geoisum  13876  geoisumr  13877  mertenslem1  13883  mertenslem2  13884  mertens  13885  risefacval2  14006  fallfacval2  14007  binomfallfaclem2  14036  bpolydiflem  14050  eff  14079  efcvg  14082  reefcl  14084  efcj  14089  eftlub  14106  effsumlt  14108  eflegeo  14118  eirrlem  14199  ruclem6  14230  dvdsmod  14305  bitsinv1lem  14358  sadcf  14370  sadadd3  14378  smupf  14395  alginv  14477  algcvg  14478  algcvga  14481  algfx  14482  eucalgcvga  14488  eucalg  14489  lcmftp  14552  phiprmpw  14667  fermltl  14675  iserodd  14728  pcpre1  14735  qexpz  14789  prmreclem4  14806  vdwapun  14867  odf1  17156  srgbinomlem4  17719  evlslem1  18681  cpmadugsumlemF  19842  dvnff  22819  dgrcl  23129  dgrub  23130  dgrlb  23132  elqaalem2  23215  elqaalem3  23216  elqaalem2OLD  23218  elqaalem3OLD  23219  geolim3  23237  tayl0  23259  dvtaylp  23267  radcnvlem1  23310  radcnvlem3  23312  radcnv0  23313  radcnvlt2  23316  pserulm  23319  psercn2  23320  pserdvlem2  23325  pserdv2  23327  abelthlem4  23331  abelthlem5  23332  abelthlem6  23333  abelthlem7  23335  abelthlem8  23336  abelthlem9  23337  cosne0  23421  logtayl  23547  leibpi  23810  leibpisum  23811  log2cnv  23812  log2tlbnd  23813  basellem3  23951  dchrptlem2  24135  bcmono  24147  lgslem4  24169  lgsne0  24203  numclwwlkovf2ex  25756  archiabllem1b  28460  oddpwdc  29139  ballotlemfval0  29280  fwddifnp1  30881  itg2addnclem2  31901  rmynn  35719  jm2.24nn  35722  jm2.17c  35725  jm2.24  35726  acongrep  35743  acongeq  35746  dvdsabsmod0OLD  35754  jm2.18  35756  jm2.23  35764  jm2.20nn  35765  jm2.27a  35773  jm2.27c  35775  rmydioph  35782  hashnzfz  36582  bccbc  36607  binomcxplemnn0  36611  binomcxplemrat  36612  binomcxplemnotnn0  36618  mccllem  37560  expfac  37621  sinaover2ne0  37626  dvnmul  37701  dvnprodlem1  37704  dvnprodlem2  37705  stoweidlem11  37754  stoweidlem26  37769  stoweidlem34  37778  stirlinglem5  37823  fourierdlem11  37863  fourierdlem12  37864  fourierdlem14  37866  fourierdlem15  37867  fourierdlem24  37876  fourierdlem25  37877  fourierdlem36  37889  fourierdlem37  37890  fourierdlem41  37894  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem64  37917  fourierdlem69  37922  fourierdlem73  37926  fourierdlem79  37932  fourierdlem81  37934  fourierdlem92  37945  fourierdlem93  37946  fourierdlem111  37964  elaa2lem  37980  elaa2lemOLD  37981  etransclem3  37985  etransclem7  37989  etransclem10  37992  etransclem24  38006  etransclem27  38009  etransclem35  38017  etransclem44  38026  etransclem46  38028  etransclem47  38029  etransclem48OLD  38030  etransclem48  38031  iccpartigtl  38550  iccpartltu  38552  iccpartgt  38554  pfxnd  38749  pfxccatin12lem1  38777  2ffzoeq  38861  0even  39522  2zrngamgm  39530  altgsumbcALT  39727  expnegico01  39908  dig0  40010  nn0sumshdiglem2  40026