Theorem 0zd 12517

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

Syntax hints:   → wi 4   ∈ wcel 2109  0cc0 11044  ℤcz 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addrcl 11105  ax-rnegex 11115  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506

This theorem is referenced by:  fzctr  13577  fzosubel3  13663  bcval5  14259  snopiswrd  14464  wrdsymb0  14490  ccatsymb  14523  swrdspsleq  14606  pfxnd  14628  pfxccatin12lem1  14669  swrdccat  14676  repswswrd  14725  eqwrds3  14903  fzomaxdiflem  15285  fsumzcl  15677  isumnn0nn  15784  climcndslem1  15791  climcnds  15793  harmonic  15801  geolim  15812  geolim2  15813  geoisum  15819  geoisumr  15820  mertenslem1  15826  mertenslem2  15827  mertens  15828  risefacval2  15952  fallfacval2  15953  binomfallfaclem2  15982  bpolydiflem  15996  eff  16023  efcvg  16027  reefcl  16029  efcj  16034  eftlub  16053  effsumlt  16055  eflegeo  16065  eirrlem  16148  ruclem6  16179  dvdsmodexp  16206  dvdsmod  16275  pwp1fsum  16337  bitsinv1lem  16387  sadcf  16399  sadadd3  16407  smupf  16424  gcdmultipled  16480  alginv  16521  algcvg  16522  algcvga  16525  algfx  16526  eucalgcvga  16532  eucalg  16533  lcmftp  16582  phiprmpw  16722  iserodd  16782  pcpre1  16789  qexpz  16848  prmreclem4  16866  vdwapun  16921  smndex2dnrinv  18818  odf1  19468  ablsimpgfindlem1  20015  srgbinomlem4  20114  pzriprnglem5  21371  pzriprnglem8  21374  pzriprnglem10  21376  pzriprnglem11  21377  pzriprng1ALT  21382  evlslem1  21965  psdmul  22029  cpmadugsumlemF  22739  dvnff  25801  dgrcl  26114  dgrub  26115  dgrlb  26117  elqaalem2  26204  elqaalem3  26205  geolim3  26223  tayl0  26245  dvtaylp  26254  radcnvlem1  26298  radcnvlem3  26300  radcnv0  26301  radcnvlt2  26304  pserulm  26307  psercn2  26308  psercn2OLD  26309  pserdvlem2  26314  pserdv2  26316  abelthlem4  26320  abelthlem5  26321  abelthlem6  26322  abelthlem7  26324  abelthlem8  26325  abelthlem9  26326  cos02pilt1  26411  cosne0  26414  logtayl  26545  leibpi  26828  leibpisum  26829  log2cnv  26830  log2tlbnd  26831  basellem3  26969  dchrptlem2  27152  bcmono  27164  lgsne0  27222  crctcshwlkn0lem3  29715  fzo0opth  32701  pfxlsw2ccat  32845  wrdt2ind  32848  gsumzrsum  32972  gsummulgc2  32973  gsumwrd2dccatlem  32979  cycpmco2lem7  33062  cyc3conja  33087  archiabllem1b  33119  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnlem4  33169  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  constrrecl  33732  constrimcl  33733  constrmulcl  33734  constrreinvcl  33735  constrinvcl  33736  constrresqrtcl  33740  constrabscl  33741  constrsqrtcl  33742  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminply  33751  cos9thpinconstrlem1  33752  oddpwdc  34318  ballotlemfval0  34460  fsum2dsub  34571  breprexplemc  34596  breprexp  34597  circlemeth  34604  fwddifnp1  36126  knoppcnlem6  36459  knoppcnlem9  36462  knoppcn  36465  knoppndvlem2  36474  knoppndvlem4  36476  knoppf  36496  itg2addnclem2  37639  lcmineqlem4  41993  lcmineqlem18  42007  aks4d1p1p2  42031  aks4d1p3  42039  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8  42048  aks4d1p9  42049  posbezout  42061  primrootspoweq0  42067  aks6d1c1  42077  aks6d1c2lem4  42088  aks6d1c2  42091  aks6d1c5lem1  42097  aks6d1c5lem2  42099  2np3bcnp1  42105  sticksstones12a  42118  sticksstones22  42129  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c6isolem1  42135  aks6d1c6lem5  42138  bcled  42139  bcle2d  42140  aks6d1c7lem1  42141  aks6d1c7lem2  42142  psrbagres  42507  evlsvvvallem  42522  selvvvval  42546  evlselvlem  42547  evlselv  42548  mhphf  42558  fltnltalem  42623  rmynn  42918  jm2.24nn  42921  jm2.17c  42924  jm2.24  42925  acongrep  42942  acongeq  42945  jm2.18  42950  jm2.23  42958  jm2.20nn  42959  jm2.27a  42967  jm2.27c  42969  rmydioph  42976  hashnzfz  44282  bccbc  44307  binomcxplemnn0  44311  binomcxplemrat  44312  binomcxplemnotnn0  44318  mccllem  45568  expfac  45628  0cnv  45713  lmbr3v  45716  sinaover2ne0  45839  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  stoweidlem11  45982  stoweidlem26  45997  stoweidlem34  46005  stirlinglem5  46049  fourierdlem11  46089  fourierdlem12  46090  fourierdlem14  46092  fourierdlem15  46093  fourierdlem24  46102  fourierdlem25  46103  fourierdlem36  46114  fourierdlem37  46115  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem64  46141  fourierdlem69  46146  fourierdlem73  46150  fourierdlem79  46156  fourierdlem81  46158  fourierdlem92  46169  fourierdlem93  46170  fourierdlem111  46188  elaa2lem  46204  etransclem3  46208  etransclem7  46212  etransclem10  46215  etransclem24  46229  etransclem27  46232  etransclem35  46240  etransclem44  46249  etransclem46  46251  etransclem47  46252  etransclem48  46253  natglobalincr  46848  2ffzoeq  47301  iccpartigtl  47397  iccpartltu  47399  iccpartgt  47401  0even  48198  2zrngamgm  48206  altgsumbcALT  48314  expnegico01  48480  dig0  48568  nn0sumshdiglem2  48584