Theorem 0zd 12261

Description: Zero is an integer, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0zd	⊢ (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 12260	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  0cc0 10802  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  fzctr  13297  fzosubel3  13376  bcval5  13960  snopiswrd  14154  wrdsymb0  14180  ccatsymb  14215  swrdspsleq  14306  pfxnd  14328  pfxccatin12lem1  14369  swrdccat  14376  repswswrd  14425  eqwrds3  14604  fzomaxdiflem  14982  fsumzcl  15375  isumnn0nn  15482  climcndslem1  15489  climcnds  15491  harmonic  15499  geolim  15510  geolim2  15511  geoisum  15517  geoisumr  15518  mertenslem1  15524  mertenslem2  15525  mertens  15526  risefacval2  15648  fallfacval2  15649  binomfallfaclem2  15678  bpolydiflem  15692  eff  15719  efcvg  15722  reefcl  15724  efcj  15729  eftlub  15746  effsumlt  15748  eflegeo  15758  eirrlem  15841  ruclem6  15872  dvdsmodexp  15899  dvdsmod  15966  pwp1fsum  16028  bitsinv1lem  16076  sadcf  16088  sadadd3  16096  smupf  16113  gcdmultipled  16170  alginv  16208  algcvg  16209  algcvga  16212  algfx  16213  eucalgcvga  16219  eucalg  16220  lcmftp  16269  phiprmpw  16405  iserodd  16464  pcpre1  16471  qexpz  16530  prmreclem4  16548  vdwapun  16603  smndex2dnrinv  18469  odf1  19084  ablsimpgfindlem1  19625  srgbinomlem4  19694  evlslem1  21202  cpmadugsumlemF  21933  dvnff  24992  dgrcl  25299  dgrub  25300  dgrlb  25302  elqaalem2  25385  elqaalem3  25386  geolim3  25404  tayl0  25426  dvtaylp  25434  radcnvlem1  25477  radcnvlem3  25479  radcnv0  25480  radcnvlt2  25483  pserulm  25486  psercn2  25487  pserdvlem2  25492  pserdv2  25494  abelthlem4  25498  abelthlem5  25499  abelthlem6  25500  abelthlem7  25502  abelthlem8  25503  abelthlem9  25504  cos02pilt1  25587  cosne0  25590  logtayl  25720  leibpi  25997  leibpisum  25998  log2cnv  25999  log2tlbnd  26000  basellem3  26137  dchrptlem2  26318  bcmono  26330  lgsne0  26388  crctcshwlkn0lem3  28078  pfxlsw2ccat  31126  wrdt2ind  31127  cycpmco2lem7  31301  cyc3conja  31326  archiabllem1b  31348  oddpwdc  32221  ballotlemfval0  32362  fsum2dsub  32487  breprexplemc  32512  breprexp  32513  circlemeth  32520  fwddifnp1  34394  knoppcnlem6  34605  knoppcnlem9  34608  knoppcn  34611  knoppndvlem2  34620  knoppndvlem4  34622  knoppf  34642  itg2addnclem2  35756  lcmineqlem4  39968  lcmineqlem18  39982  aks4d1p1p2  40006  aks4d1p3  40014  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  2np3bcnp1  40028  sticksstones12a  40041  sticksstones22  40052  metakunt29  40081  metakunt30  40082  metakunt32  40084  metakunt33  40085  fltnltalem  40415  rmynn  40694  jm2.24nn  40697  jm2.17c  40700  jm2.24  40701  acongrep  40718  acongeq  40721  jm2.18  40726  jm2.23  40734  jm2.20nn  40735  jm2.27a  40743  jm2.27c  40745  rmydioph  40752  hashnzfz  41827  bccbc  41852  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemnotnn0  41863  mccllem  43028  expfac  43088  0cnv  43173  lmbr3v  43176  sinaover2ne0  43299  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  stoweidlem11  43442  stoweidlem26  43457  stoweidlem34  43465  stirlinglem5  43509  fourierdlem11  43549  fourierdlem12  43550  fourierdlem14  43552  fourierdlem15  43553  fourierdlem24  43562  fourierdlem25  43563  fourierdlem36  43574  fourierdlem37  43575  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem64  43601  fourierdlem69  43606  fourierdlem73  43610  fourierdlem79  43616  fourierdlem81  43618  fourierdlem92  43629  fourierdlem93  43630  fourierdlem111  43648  elaa2lem  43664  etransclem3  43668  etransclem7  43672  etransclem10  43675  etransclem24  43689  etransclem27  43692  etransclem35  43700  etransclem44  43709  etransclem46  43711  etransclem47  43712  etransclem48  43713  2ffzoeq  44708  iccpartigtl  44763  iccpartltu  44765  iccpartgt  44767  0even  45377  2zrngamgm  45385  altgsumbcALT  45577  expnegico01  45747  dig0  45840  nn0sumshdiglem2  45856