Theorem 0zd 10977

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

Syntax hints:   -> wi 4   e. wcel 1897   0cc0 9564   ZZcz 10965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-i2m1 9632  ax-1ne0 9633  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-iota 5564  df-fv 5608  df-ov 6317  df-neg 9888  df-z 10966

This theorem is referenced by:  fzctr  11932  fzosubel3  12005  bcval5  12534  wrdsymb0  12736  ccatsymb  12762  swrdspsleq  12841  swrdccatin12lem2b  12878  swrdccat  12885  repswswrd  12923  fzomaxdiflem  13453  fsumzcl  13849  isumnn0nn  13948  climcndslem1  13955  climcnds  13957  harmonic  13965  geolim  13974  geolim2  13975  geoisum  13981  geoisumr  13982  mertenslem1  13988  mertenslem2  13989  mertens  13990  risefacval2  14111  fallfacval2  14112  binomfallfaclem2  14141  bpolydiflem  14155  eff  14184  efcvg  14187  reefcl  14189  efcj  14194  eftlub  14211  effsumlt  14213  eflegeo  14223  eirrlem  14304  ruclem6  14335  dvdsmod  14410  bitsinv1lem  14463  sadcf  14475  sadadd3  14483  smupf  14500  alginv  14582  algcvg  14583  algcvga  14586  algfx  14587  eucalgcvga  14593  eucalg  14594  lcmftp  14657  phiprmpw  14772  fermltl  14780  iserodd  14833  pcpre1  14840  qexpz  14894  prmreclem4  14911  vdwapun  14972  odf1  17261  srgbinomlem4  17824  evlslem1  18786  cpmadugsumlemF  19948  dvnff  22925  dgrcl  23235  dgrub  23236  dgrlb  23238  elqaalem2  23321  elqaalem3  23322  elqaalem2OLD  23324  elqaalem3OLD  23325  geolim3  23343  tayl0  23365  dvtaylp  23373  radcnvlem1  23416  radcnvlem3  23418  radcnv0  23419  radcnvlt2  23422  pserulm  23425  psercn2  23426  pserdvlem2  23431  pserdv2  23433  abelthlem4  23437  abelthlem5  23438  abelthlem6  23439  abelthlem7  23441  abelthlem8  23442  abelthlem9  23443  cosne0  23527  logtayl  23653  leibpi  23916  leibpisum  23917  log2cnv  23918  log2tlbnd  23919  basellem3  24057  dchrptlem2  24241  bcmono  24253  lgslem4  24275  lgsne0  24309  numclwwlkovf2ex  25862  archiabllem1b  28557  oddpwdc  29235  ballotlemfval0  29376  fwddifnp1  30980  itg2addnclem2  32038  rmynn  35850  jm2.24nn  35853  jm2.17c  35856  jm2.24  35857  acongrep  35874  acongeq  35877  dvdsabsmod0OLD  35885  jm2.18  35887  jm2.23  35895  jm2.20nn  35896  jm2.27a  35904  jm2.27c  35906  rmydioph  35913  hashnzfz  36712  bccbc  36737  binomcxplemnn0  36741  binomcxplemrat  36742  binomcxplemnotnn0  36748  mccllem  37714  expfac  37775  sinaover2ne0  37780  dvnmul  37855  dvnprodlem1  37858  dvnprodlem2  37859  stoweidlem11  37908  stoweidlem26  37923  stoweidlem34  37932  stirlinglem5  37977  fourierdlem11  38017  fourierdlem12  38018  fourierdlem14  38020  fourierdlem15  38021  fourierdlem24  38030  fourierdlem25  38031  fourierdlem36  38043  fourierdlem37  38044  fourierdlem41  38048  fourierdlem48  38055  fourierdlem49  38056  fourierdlem50  38057  fourierdlem64  38071  fourierdlem69  38076  fourierdlem73  38080  fourierdlem79  38086  fourierdlem81  38088  fourierdlem92  38099  fourierdlem93  38100  fourierdlem111  38118  elaa2lem  38134  elaa2lemOLD  38135  etransclem3  38139  etransclem7  38143  etransclem10  38146  etransclem24  38160  etransclem27  38163  etransclem35  38171  etransclem44  38180  etransclem46  38182  etransclem47  38183  etransclem48OLD  38184  etransclem48  38185  iccpartigtl  38774  iccpartltu  38776  iccpartgt  38778  pfxnd  38975  pfxccatin12lem1  39003  2ffzoeq  39105  0even  40203  2zrngamgm  40211  altgsumbcALT  40406  expnegico01  40587  dig0  40689  nn0sumshdiglem2  40705