Theorem 0zd 12598

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

Syntax hints:   → wi 4   ∈ wcel 2108  0cc0 11127  ℤcz 12586

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addrcl 11188  ax-rnegex 11198  ax-cnre 11200

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-neg 11467  df-z 12587

This theorem is referenced by:  fzctr  13655  fzosubel3  13740  bcval5  14334  snopiswrd  14539  wrdsymb0  14565  ccatsymb  14598  swrdspsleq  14681  pfxnd  14703  pfxccatin12lem1  14744  swrdccat  14751  repswswrd  14800  eqwrds3  14978  fzomaxdiflem  15359  fsumzcl  15749  isumnn0nn  15856  climcndslem1  15863  climcnds  15865  harmonic  15873  geolim  15884  geolim2  15885  geoisum  15891  geoisumr  15892  mertenslem1  15898  mertenslem2  15899  mertens  15900  risefacval2  16024  fallfacval2  16025  binomfallfaclem2  16054  bpolydiflem  16068  eff  16095  efcvg  16099  reefcl  16101  efcj  16106  eftlub  16125  effsumlt  16127  eflegeo  16137  eirrlem  16220  ruclem6  16251  dvdsmodexp  16278  dvdsmod  16346  pwp1fsum  16408  bitsinv1lem  16458  sadcf  16470  sadadd3  16478  smupf  16495  gcdmultipled  16551  alginv  16592  algcvg  16593  algcvga  16596  algfx  16597  eucalgcvga  16603  eucalg  16604  lcmftp  16653  phiprmpw  16793  iserodd  16853  pcpre1  16860  qexpz  16919  prmreclem4  16937  vdwapun  16992  smndex2dnrinv  18891  odf1  19541  ablsimpgfindlem1  20088  srgbinomlem4  20187  pzriprnglem5  21444  pzriprnglem8  21447  pzriprnglem10  21449  pzriprnglem11  21450  pzriprng1ALT  21455  evlslem1  22038  psdmul  22102  cpmadugsumlemF  22812  dvnff  25875  dgrcl  26188  dgrub  26189  dgrlb  26191  elqaalem2  26278  elqaalem3  26279  geolim3  26297  tayl0  26319  dvtaylp  26328  radcnvlem1  26372  radcnvlem3  26374  radcnv0  26375  radcnvlt2  26378  pserulm  26381  psercn2  26382  psercn2OLD  26383  pserdvlem2  26388  pserdv2  26390  abelthlem4  26394  abelthlem5  26395  abelthlem6  26396  abelthlem7  26398  abelthlem8  26399  abelthlem9  26400  cos02pilt1  26485  cosne0  26488  logtayl  26619  leibpi  26902  leibpisum  26903  log2cnv  26904  log2tlbnd  26905  basellem3  27043  dchrptlem2  27226  bcmono  27238  lgsne0  27296  crctcshwlkn0lem3  29740  fzo0opth  32728  pfxlsw2ccat  32872  wrdt2ind  32875  gsumzrsum  32999  gsummulgc2  33000  gsumwrd2dccatlem  33006  cycpmco2lem7  33089  cyc3conja  33114  archiabllem1b  33136  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  constrrecl  33749  constrimcl  33750  constrmulcl  33751  constrreinvcl  33752  constrinvcl  33753  constrresqrtcl  33757  constrabscl  33758  constrsqrtcl  33759  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminply  33768  cos9thpinconstrlem1  33769  oddpwdc  34332  ballotlemfval0  34474  fsum2dsub  34585  breprexplemc  34610  breprexp  34611  circlemeth  34618  fwddifnp1  36129  knoppcnlem6  36462  knoppcnlem9  36465  knoppcn  36468  knoppndvlem2  36477  knoppndvlem4  36479  knoppf  36499  itg2addnclem2  37642  lcmineqlem4  41991  lcmineqlem18  42005  aks4d1p1p2  42029  aks4d1p3  42037  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  posbezout  42059  primrootspoweq0  42065  aks6d1c1  42075  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5lem1  42095  aks6d1c5lem2  42097  2np3bcnp1  42103  sticksstones12a  42116  sticksstones22  42127  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6lem5  42136  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  aks6d1c7lem2  42140  metakunt29  42192  metakunt30  42193  metakunt32  42195  metakunt33  42196  psrbagres  42516  evlsvvvallem  42531  selvvvval  42555  evlselvlem  42556  evlselv  42557  mhphf  42567  fltnltalem  42632  rmynn  42927  jm2.24nn  42930  jm2.17c  42933  jm2.24  42934  acongrep  42951  acongeq  42954  jm2.18  42959  jm2.23  42967  jm2.20nn  42968  jm2.27a  42976  jm2.27c  42978  rmydioph  42985  hashnzfz  44292  bccbc  44317  binomcxplemnn0  44321  binomcxplemrat  44322  binomcxplemnotnn0  44328  mccllem  45574  expfac  45634  0cnv  45719  lmbr3v  45722  sinaover2ne0  45845  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  stoweidlem11  45988  stoweidlem26  46003  stoweidlem34  46011  stirlinglem5  46055  fourierdlem11  46095  fourierdlem12  46096  fourierdlem14  46098  fourierdlem15  46099  fourierdlem24  46108  fourierdlem25  46109  fourierdlem36  46120  fourierdlem37  46121  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem64  46147  fourierdlem69  46152  fourierdlem73  46156  fourierdlem79  46162  fourierdlem81  46164  fourierdlem92  46175  fourierdlem93  46176  fourierdlem111  46194  elaa2lem  46210  etransclem3  46214  etransclem7  46218  etransclem10  46221  etransclem24  46235  etransclem27  46238  etransclem35  46246  etransclem44  46255  etransclem46  46257  etransclem47  46258  etransclem48  46259  natglobalincr  46854  2ffzoeq  47304  iccpartigtl  47385  iccpartltu  47387  iccpartgt  47389  0even  48160  2zrngamgm  48168  altgsumbcALT  48276  expnegico01  48442  dig0  48534  nn0sumshdiglem2  48550