Theorem 0zd 12527

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

Syntax hints:   → wi 4   ∈ wcel 2114  0cc0 11029  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-neg 11371  df-z 12516

This theorem is referenced by:  fzctr  13585  fzosubel3  13672  bcval5  14271  snopiswrd  14476  wrdsymb0  14502  ccatsymb  14536  swrdspsleq  14619  pfxnd  14641  pfxccatin12lem1  14681  swrdccat  14688  repswswrd  14737  eqwrds3  14914  fzomaxdiflem  15296  fsumzcl  15688  isumnn0nn  15798  climcndslem1  15805  climcnds  15807  harmonic  15815  geolim  15826  geolim2  15827  geoisum  15833  geoisumr  15834  mertenslem1  15840  mertenslem2  15841  mertens  15842  risefacval2  15966  fallfacval2  15967  binomfallfaclem2  15996  bpolydiflem  16010  eff  16037  efcvg  16041  reefcl  16043  efcj  16048  eftlub  16067  effsumlt  16069  eflegeo  16079  eirrlem  16162  ruclem6  16193  dvdsmodexp  16220  dvdsmod  16289  pwp1fsum  16351  bitsinv1lem  16401  sadcf  16413  sadadd3  16421  smupf  16438  gcdmultipled  16494  alginv  16535  algcvg  16536  algcvga  16539  algfx  16540  eucalgcvga  16546  eucalg  16547  lcmftp  16596  phiprmpw  16737  iserodd  16797  pcpre1  16804  qexpz  16863  prmreclem4  16881  vdwapun  16936  chnpolfz  18590  smndex2dnrinv  18877  odf1  19528  ablsimpgfindlem1  20075  srgbinomlem4  20201  pzriprnglem5  21475  pzriprnglem8  21478  pzriprnglem10  21480  pzriprnglem11  21481  pzriprng1ALT  21486  evlslem1  22070  evlsvvvallem  22079  psdmul  22142  cpmadugsumlemF  22851  dvnff  25900  dgrcl  26208  dgrub  26209  dgrlb  26211  elqaalem2  26297  elqaalem3  26298  geolim3  26316  tayl0  26338  dvtaylp  26347  radcnvlem1  26391  radcnvlem3  26393  radcnv0  26394  radcnvlt2  26397  pserulm  26400  psercn2  26401  pserdvlem2  26406  pserdv2  26408  abelthlem4  26412  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  abelthlem8  26417  abelthlem9  26418  cos02pilt1  26503  cosne0  26506  logtayl  26637  leibpi  26919  leibpisum  26920  log2cnv  26921  log2tlbnd  26922  basellem3  27060  dchrptlem2  27242  bcmono  27254  lgsne0  27312  crctcshwlkn0lem3  29895  fzo0opth  32891  pfxlsw2ccat  33025  wrdt2ind  33028  gsumzrsum  33141  gsummulgc2  33142  gsumwrd2dccatlem  33153  cycpmco2lem7  33208  cyc3conja  33233  archiabllem1b  33268  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  esplyfval0  33723  esplyfval2  33724  esplympl  33726  esplyfval3  33731  vietadeg1  33737  constrrecl  33929  constrimcl  33930  constrmulcl  33931  constrreinvcl  33932  constrinvcl  33933  constrresqrtcl  33937  constrabscl  33938  constrsqrtcl  33939  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpiminply  33948  cos9thpinconstrlem1  33949  oddpwdc  34514  ballotlemfval0  34656  fsum2dsub  34767  breprexplemc  34792  breprexp  34793  circlemeth  34800  fwddifnp1  36363  knoppcnlem6  36774  knoppcnlem9  36777  knoppcn  36780  knoppndvlem2  36789  knoppndvlem4  36791  knoppf  36811  itg2addnclem2  38007  lcmineqlem4  42485  lcmineqlem18  42499  aks4d1p1p2  42523  aks4d1p3  42531  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  primrootspoweq0  42559  aks6d1c1  42569  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5lem1  42589  aks6d1c5lem2  42591  2np3bcnp1  42597  sticksstones12a  42610  sticksstones22  42621  aks6d1c6lem3  42625  aks6d1c6lem4  42626  aks6d1c6isolem1  42627  aks6d1c6lem5  42630  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7lem2  42634  psrbagres  43003  selvvvval  43032  evlselvlem  43033  evlselv  43034  mhphf  43044  fltnltalem  43109  rmynn  43402  jm2.24nn  43405  jm2.17c  43408  jm2.24  43409  acongrep  43426  acongeq  43429  jm2.18  43434  jm2.23  43442  jm2.20nn  43443  jm2.27a  43451  jm2.27c  43453  rmydioph  43460  hashnzfz  44765  bccbc  44790  binomcxplemnn0  44794  binomcxplemrat  44795  binomcxplemnotnn0  44801  mccllem  46045  expfac  46103  0cnv  46188  lmbr3v  46191  sinaover2ne0  46314  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  stoweidlem11  46457  stoweidlem26  46472  stoweidlem34  46480  stirlinglem5  46524  fourierdlem11  46564  fourierdlem12  46565  fourierdlem14  46567  fourierdlem15  46568  fourierdlem24  46577  fourierdlem25  46578  fourierdlem36  46589  fourierdlem37  46590  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem64  46616  fourierdlem69  46621  fourierdlem73  46625  fourierdlem79  46631  fourierdlem81  46633  fourierdlem92  46644  fourierdlem93  46645  fourierdlem111  46663  elaa2lem  46679  etransclem3  46683  etransclem7  46687  etransclem10  46690  etransclem24  46704  etransclem27  46707  etransclem35  46715  etransclem44  46724  etransclem46  46726  etransclem47  46727  etransclem48  46728  natglobalincr  47323  chnsubseqwl  47325  chnsubseq  47326  2ffzoeq  47788  iccpartigtl  47895  iccpartltu  47897  iccpartgt  47899  0even  48725  2zrngamgm  48733  altgsumbcALT  48841  expnegico01  49006  dig0  49094  nn0sumshdiglem2  49110