Theorem 0zd 12501

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

Syntax hints:   → wi 4   ∈ wcel 2109  0cc0 11028  ℤcz 12489

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 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-neg 11368  df-z 12490

This theorem is referenced by:  fzctr  13561  fzosubel3  13647  bcval5  14243  snopiswrd  14448  wrdsymb0  14474  ccatsymb  14507  swrdspsleq  14590  pfxnd  14612  pfxccatin12lem1  14652  swrdccat  14659  repswswrd  14708  eqwrds3  14886  fzomaxdiflem  15268  fsumzcl  15660  isumnn0nn  15767  climcndslem1  15774  climcnds  15776  harmonic  15784  geolim  15795  geolim2  15796  geoisum  15802  geoisumr  15803  mertenslem1  15809  mertenslem2  15810  mertens  15811  risefacval2  15935  fallfacval2  15936  binomfallfaclem2  15965  bpolydiflem  15979  eff  16006  efcvg  16010  reefcl  16012  efcj  16017  eftlub  16036  effsumlt  16038  eflegeo  16048  eirrlem  16131  ruclem6  16162  dvdsmodexp  16189  dvdsmod  16258  pwp1fsum  16320  bitsinv1lem  16370  sadcf  16382  sadadd3  16390  smupf  16407  gcdmultipled  16463  alginv  16504  algcvg  16505  algcvga  16508  algfx  16509  eucalgcvga  16515  eucalg  16516  lcmftp  16565  phiprmpw  16705  iserodd  16765  pcpre1  16772  qexpz  16831  prmreclem4  16849  vdwapun  16904  smndex2dnrinv  18807  odf1  19459  ablsimpgfindlem1  20006  srgbinomlem4  20132  pzriprnglem5  21410  pzriprnglem8  21413  pzriprnglem10  21415  pzriprnglem11  21416  pzriprng1ALT  21421  evlslem1  22005  psdmul  22069  cpmadugsumlemF  22779  dvnff  25841  dgrcl  26154  dgrub  26155  dgrlb  26157  elqaalem2  26244  elqaalem3  26245  geolim3  26263  tayl0  26285  dvtaylp  26294  radcnvlem1  26338  radcnvlem3  26340  radcnv0  26341  radcnvlt2  26344  pserulm  26347  psercn2  26348  psercn2OLD  26349  pserdvlem2  26354  pserdv2  26356  abelthlem4  26360  abelthlem5  26361  abelthlem6  26362  abelthlem7  26364  abelthlem8  26365  abelthlem9  26366  cos02pilt1  26451  cosne0  26454  logtayl  26585  leibpi  26868  leibpisum  26869  log2cnv  26870  log2tlbnd  26871  basellem3  27009  dchrptlem2  27192  bcmono  27204  lgsne0  27262  crctcshwlkn0lem3  29775  fzo0opth  32761  pfxlsw2ccat  32905  wrdt2ind  32908  gsumzrsum  33025  gsummulgc2  33026  gsumwrd2dccatlem  33032  cycpmco2lem7  33087  cyc3conja  33112  archiabllem1b  33147  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  constrrecl  33738  constrimcl  33739  constrmulcl  33740  constrreinvcl  33741  constrinvcl  33742  constrresqrtcl  33746  constrabscl  33747  constrsqrtcl  33748  cos9thpiminplylem1  33751  cos9thpiminplylem2  33752  cos9thpiminply  33757  cos9thpinconstrlem1  33758  oddpwdc  34324  ballotlemfval0  34466  fsum2dsub  34577  breprexplemc  34602  breprexp  34603  circlemeth  34610  fwddifnp1  36141  knoppcnlem6  36474  knoppcnlem9  36477  knoppcn  36480  knoppndvlem2  36489  knoppndvlem4  36491  knoppf  36511  itg2addnclem2  37654  lcmineqlem4  42008  lcmineqlem18  42022  aks4d1p1p2  42046  aks4d1p3  42054  aks4d1p7d1  42058  aks4d1p7  42059  aks4d1p8  42063  aks4d1p9  42064  posbezout  42076  primrootspoweq0  42082  aks6d1c1  42092  aks6d1c2lem4  42103  aks6d1c2  42106  aks6d1c5lem1  42112  aks6d1c5lem2  42114  2np3bcnp1  42120  sticksstones12a  42133  sticksstones22  42144  aks6d1c6lem3  42148  aks6d1c6lem4  42149  aks6d1c6isolem1  42150  aks6d1c6lem5  42153  bcled  42154  bcle2d  42155  aks6d1c7lem1  42156  aks6d1c7lem2  42157  psrbagres  42522  evlsvvvallem  42537  selvvvval  42561  evlselvlem  42562  evlselv  42563  mhphf  42573  fltnltalem  42638  rmynn  42932  jm2.24nn  42935  jm2.17c  42938  jm2.24  42939  acongrep  42956  acongeq  42959  jm2.18  42964  jm2.23  42972  jm2.20nn  42973  jm2.27a  42981  jm2.27c  42983  rmydioph  42990  hashnzfz  44296  bccbc  44321  binomcxplemnn0  44325  binomcxplemrat  44326  binomcxplemnotnn0  44332  mccllem  45582  expfac  45642  0cnv  45727  lmbr3v  45730  sinaover2ne0  45853  dvnmul  45928  dvnprodlem1  45931  dvnprodlem2  45932  stoweidlem11  45996  stoweidlem26  46011  stoweidlem34  46019  stirlinglem5  46063  fourierdlem11  46103  fourierdlem12  46104  fourierdlem14  46106  fourierdlem15  46107  fourierdlem24  46116  fourierdlem25  46117  fourierdlem36  46128  fourierdlem37  46129  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem64  46155  fourierdlem69  46160  fourierdlem73  46164  fourierdlem79  46170  fourierdlem81  46172  fourierdlem92  46183  fourierdlem93  46184  fourierdlem111  46202  elaa2lem  46218  etransclem3  46222  etransclem7  46226  etransclem10  46229  etransclem24  46243  etransclem27  46246  etransclem35  46254  etransclem44  46263  etransclem46  46265  etransclem47  46266  etransclem48  46267  natglobalincr  46862  2ffzoeq  47315  iccpartigtl  47411  iccpartltu  47413  iccpartgt  47415  0even  48225  2zrngamgm  48233  altgsumbcALT  48341  expnegico01  48507  dig0  48595  nn0sumshdiglem2  48611