Theorem 0zd 12340

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 12339	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2107  0cc0 10880  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-addrcl 10941  ax-rnegex 10951  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-neg 11217  df-z 12329

This theorem is referenced by:  fzctr  13377  fzosubel3  13457  bcval5  14041  snopiswrd  14235  wrdsymb0  14261  ccatsymb  14296  swrdspsleq  14387  pfxnd  14409  pfxccatin12lem1  14450  swrdccat  14457  repswswrd  14506  eqwrds3  14685  fzomaxdiflem  15063  fsumzcl  15456  isumnn0nn  15563  climcndslem1  15570  climcnds  15572  harmonic  15580  geolim  15591  geolim2  15592  geoisum  15598  geoisumr  15599  mertenslem1  15605  mertenslem2  15606  mertens  15607  risefacval2  15729  fallfacval2  15730  binomfallfaclem2  15759  bpolydiflem  15773  eff  15800  efcvg  15803  reefcl  15805  efcj  15810  eftlub  15827  effsumlt  15829  eflegeo  15839  eirrlem  15922  ruclem6  15953  dvdsmodexp  15980  dvdsmod  16047  pwp1fsum  16109  bitsinv1lem  16157  sadcf  16169  sadadd3  16177  smupf  16194  gcdmultipled  16251  alginv  16289  algcvg  16290  algcvga  16293  algfx  16294  eucalgcvga  16300  eucalg  16301  lcmftp  16350  phiprmpw  16486  iserodd  16545  pcpre1  16552  qexpz  16611  prmreclem4  16629  vdwapun  16684  smndex2dnrinv  18563  odf1  19178  ablsimpgfindlem1  19719  srgbinomlem4  19788  evlslem1  21301  cpmadugsumlemF  22034  dvnff  25096  dgrcl  25403  dgrub  25404  dgrlb  25406  elqaalem2  25489  elqaalem3  25490  geolim3  25508  tayl0  25530  dvtaylp  25538  radcnvlem1  25581  radcnvlem3  25583  radcnv0  25584  radcnvlt2  25587  pserulm  25590  psercn2  25591  pserdvlem2  25596  pserdv2  25598  abelthlem4  25602  abelthlem5  25603  abelthlem6  25604  abelthlem7  25606  abelthlem8  25607  abelthlem9  25608  cos02pilt1  25691  cosne0  25694  logtayl  25824  leibpi  26101  leibpisum  26102  log2cnv  26103  log2tlbnd  26104  basellem3  26241  dchrptlem2  26422  bcmono  26434  lgsne0  26492  crctcshwlkn0lem3  28186  pfxlsw2ccat  31233  wrdt2ind  31234  cycpmco2lem7  31408  cyc3conja  31433  archiabllem1b  31455  oddpwdc  32330  ballotlemfval0  32471  fsum2dsub  32596  breprexplemc  32621  breprexp  32622  circlemeth  32629  fwddifnp1  34476  knoppcnlem6  34687  knoppcnlem9  34690  knoppcn  34693  knoppndvlem2  34702  knoppndvlem4  34704  knoppf  34724  itg2addnclem2  35838  lcmineqlem4  40047  lcmineqlem18  40061  aks4d1p1p2  40085  aks4d1p3  40093  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  aks4d1p9  40103  2np3bcnp1  40107  sticksstones12a  40120  sticksstones22  40131  metakunt29  40160  metakunt30  40161  metakunt32  40163  metakunt33  40164  fltnltalem  40506  rmynn  40785  jm2.24nn  40788  jm2.17c  40791  jm2.24  40792  acongrep  40809  acongeq  40812  jm2.18  40817  jm2.23  40825  jm2.20nn  40826  jm2.27a  40834  jm2.27c  40836  rmydioph  40843  hashnzfz  41945  bccbc  41970  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemnotnn0  41981  mccllem  43145  expfac  43205  0cnv  43290  lmbr3v  43293  sinaover2ne0  43416  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  stoweidlem11  43559  stoweidlem26  43574  stoweidlem34  43582  stirlinglem5  43626  fourierdlem11  43666  fourierdlem12  43667  fourierdlem14  43669  fourierdlem15  43670  fourierdlem24  43679  fourierdlem25  43680  fourierdlem36  43691  fourierdlem37  43692  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem64  43718  fourierdlem69  43723  fourierdlem73  43727  fourierdlem79  43733  fourierdlem81  43735  fourierdlem92  43746  fourierdlem93  43747  fourierdlem111  43765  elaa2lem  43781  etransclem3  43785  etransclem7  43789  etransclem10  43792  etransclem24  43806  etransclem27  43809  etransclem35  43817  etransclem44  43826  etransclem46  43828  etransclem47  43829  etransclem48  43830  2ffzoeq  44831  iccpartigtl  44886  iccpartltu  44888  iccpartgt  44890  0even  45500  2zrngamgm  45508  altgsumbcALT  45700  expnegico01  45870  dig0  45963  nn0sumshdiglem2  45979  natglobalincr  46523