Theorem 0zd 12709

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  0cc0 11204  ℤcz 12697

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11262  ax-addrcl 11265  ax-rnegex 11275  ax-cnre 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424  df-neg 11548  df-z 12698

This theorem is used by:  fzctr  13778  fzosubel3  13865  bcval5  14466  snopiswrd  14672  wrdsymb0  14698  ccatsymb  14732  swrdspsleq  14820  pfxnd  14842  pfxccatin12lem1  14882  swrdccat  14889  repswswrd  14940  eqwrds3  15120  fzomaxdiflem  15516  fsumzcl  15907  isumnn0nn  16017  climcndslem1  16024  climcnds  16026  harmonic  16034  geolim  16045  geolim2  16046  geoisum  16052  geoisumr  16053  mertenslem1  16059  mertenslem2  16060  mertens  16061  risefacval2  16183  fallfacval2  16184  binomfallfaclem2  16212  bpolydiflem  16226  eff  16253  efcvg  16257  reefcl  16259  efcj  16264  eftlub  16283  effsumlt  16285  eflegeo  16295  eirrlem  16378  ruclem6  16409  dvdsmodexp  16436  dvdsmod  16505  pwp1fsum  16567  bitsinv1lem  16617  sadcf  16629  sadadd3  16637  smupf  16654  gcdmultipled  16713  alginv  16756  algcvg  16757  algcvga  16760  algfx  16761  eucalgcvga  16767  eucalg  16768  lcmftp  16817  phiprmpw  16959  iserodd  17019  pcpre1  17026  qexpz  17085  prmreclem4  17103  vdwapun  17158  chnpolfz  18813  smndex2dnrinv  19120  odf1  19782  ablsimpgfindlem1  20329  srgbinomlem4  20461  pzriprnglem5  21797  pzriprnglem8  21800  pzriprnglem10  21802  pzriprnglem11  21803  pzriprng1ALT  21808  psrbagres  22244  evlslem1  22397  evlsvvvallem  22406  selvvvval  22457  psdmul  22493  cpmadugsumlemF  23200  dvnff  26249  dgrcl  26558  dgrub  26559  dgrlb  26561  elqaalem2  26649  elqaalem3  26650  geolim3  26672  tayl0  26695  dvtaylp  26703  radcnvlem1  26746  radcnvlem3  26748  radcnv0  26749  radcnvlt2  26752  pserulm  26755  psercn2  26756  pserdvlem2  26761  pserdv2  26763  abelthlem4  26767  abelthlem5  26768  abelthlem6  26769  abelthlem7  26771  abelthlem8  26772  abelthlem9  26773  cos02pilt1  26860  cosne0  26863  logtayl  26994  leibpi  27276  leibpisum  27277  log2cnv  27278  log2tlbnd  27279  basellem3  27416  dchrptlem2  27598  bcmono  27610  lgsne0  27668  crctcshwlkn0lem3  30407  fzo0opth  33442  pfxlsw2ccat  33560  wrdt2ind  33563  gsumzrsum  33673  gsummulgc2  33674  gsumwrd2dccatlem  33685  cycpmco2lem7  33740  cyc3conja  33765  archiabllem1b  33800  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem3  33852  elrgspnlem4  33853  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  selvply1rhmlemb  34198  esplyfval0  34243  esplyfval2  34244  esplympl  34246  esplyfval3  34251  vietadeg1  34257  constrrecl  34448  constrimcl  34449  constrmulcl  34450  constrreinvcl  34451  constrinvcl  34452  constrresqrtcl  34456  constrabscl  34457  constrsqrtcl  34458  cos9thpiminplylem1  34461  cos9thpiminplylem2  34462  cos9thpiminply  34467  cos9thpinconstrlem1  34468  oddpwdc  35033  ballotlemfval0  35175  fsum2dsub  35283  breprexplemc  35308  breprexp  35309  circlemeth  35316  fwddifnp1  37023  knoppcnlem6  37457  knoppcnlem9  37460  knoppcn  37463  knoppndvlem2  37472  knoppndvlem4  37474  knoppf  37494  itg2addnclem2  38684  lcmineqlem4  43176  lcmineqlem18  43190  aks4d1p1p2  43214  aks4d1p3  43222  aks4d1p7d1  43226  aks4d1p7  43227  aks4d1p8  43231  aks4d1p9  43232  posbezout  43244  primrootspoweq0  43250  aks6d1c1  43260  aks6d1c2lem4  43271  aks6d1c2  43274  aks6d1c5lem1  43280  aks6d1c5lem2  43282  2np3bcnp1  43288  sticksstones12a  43301  sticksstones22  43312  aks6d1c6lem3  43316  aks6d1c6lem4  43317  aks6d1c6isolem1  43318  aks6d1c6lem5  43321  bcled  43322  bcle2d  43323  aks6d1c7lem1  43324  aks6d1c7lem2  43325  evlselvlem  43710  evlselv  43711  mhphf  43719  fltnltalem  43767  rmynn  44057  jm2.24nn  44060  jm2.17c  44063  jm2.24  44064  acongrep  44081  acongeq  44084  jm2.18  44089  jm2.23  44097  jm2.20nn  44098  jm2.27a  44106  jm2.27c  44108  rmydioph  44115  hashnzfz  45398  bccbc  45423  binomcxplemnn0  45427  binomcxplemrat  45428  binomcxplemnotnn0  45434  mccllem  46703  expfac  46761  0cnv  46846  lmbr3v  46849  sinaover2ne0  46972  dvnmul  47047  dvnprodlem1  47050  dvnprodlem2  47051  stoweidlem11  47115  stoweidlem26  47130  stoweidlem34  47138  stirlinglem5  47182  fourierdlem11  47222  fourierdlem12  47223  fourierdlem14  47225  fourierdlem15  47226  fourierdlem24  47235  fourierdlem25  47236  fourierdlem36  47247  fourierdlem37  47248  fourierdlem41  47252  fourierdlem48  47258  fourierdlem49  47259  fourierdlem50  47260  fourierdlem64  47274  fourierdlem69  47279  fourierdlem73  47283  fourierdlem79  47289  fourierdlem81  47291  fourierdlem92  47302  fourierdlem93  47303  fourierdlem111  47321  elaa2lem  47337  etransclem3  47341  etransclem7  47345  etransclem10  47348  etransclem24  47362  etransclem27  47365  etransclem35  47373  etransclem44  47382  etransclem46  47384  etransclem47  47385  etransclem48  47386  chnsubseqwl  47983  chnsubseq  47984  2ffzoeq  48492  iccpartigtl  48599  iccpartltu  48601  iccpartgt  48603  0even  49428  2zrngamgm  49436  altgsumbcALT  49559  expnegico01  49724  dig0  49812  nn0sumshdiglem2  49828