Theorem 0zd 12604

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

Syntax hints:   → wi 4   ∈ wcel 2143  0cc0 11101  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-addrcl 11162  ax-rnegex 11172  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-neg 11445  df-z 12593

This theorem is referenced by:  fzctr  13670  fzosubel3  13757  bcval5  14356  snopiswrd  14562  wrdsymb0  14588  ccatsymb  14622  swrdspsleq  14705  pfxnd  14727  pfxccatin12lem1  14767  swrdccat  14774  repswswrd  14823  eqwrds3  15000  fzomaxdiflem  15396  fsumzcl  15788  isumnn0nn  15898  climcndslem1  15905  climcnds  15907  harmonic  15915  geolim  15926  geolim2  15927  geoisum  15933  geoisumr  15934  mertenslem1  15940  mertenslem2  15941  mertens  15942  risefacval2  16066  fallfacval2  16067  binomfallfaclem2  16095  bpolydiflem  16109  eff  16136  efcvg  16140  reefcl  16142  efcj  16147  eftlub  16166  effsumlt  16168  eflegeo  16178  eirrlem  16261  ruclem6  16292  dvdsmodexp  16319  dvdsmod  16388  pwp1fsum  16450  bitsinv1lem  16500  sadcf  16512  sadadd3  16520  smupf  16537  gcdmultipled  16593  alginv  16634  algcvg  16635  algcvga  16638  algfx  16639  eucalgcvga  16645  eucalg  16646  lcmftp  16695  phiprmpw  16836  iserodd  16896  pcpre1  16903  qexpz  16962  prmreclem4  16980  vdwapun  17035  chnpolfz  18690  smndex2dnrinv  18978  odf1  19633  ablsimpgfindlem1  20180  srgbinomlem4  20312  pzriprnglem5  21616  pzriprnglem8  21619  pzriprnglem10  21621  pzriprnglem11  21622  pzriprng1ALT  21627  psrbagres  22061  evlslem1  22214  evlsvvvallem  22223  selvvvval  22274  psdmul  22310  cpmadugsumlemF  23014  dvnff  26063  dgrcl  26371  dgrub  26372  dgrlb  26374  elqaalem2  26462  elqaalem3  26463  geolim3  26483  tayl0  26506  dvtaylp  26514  radcnvlem1  26557  radcnvlem3  26559  radcnv0  26560  radcnvlt2  26563  pserulm  26566  psercn2  26567  pserdvlem2  26572  pserdv2  26574  abelthlem4  26578  abelthlem5  26579  abelthlem6  26580  abelthlem7  26582  abelthlem8  26583  abelthlem9  26584  cos02pilt1  26672  cosne0  26675  logtayl  26806  leibpi  27088  leibpisum  27089  log2cnv  27090  log2tlbnd  27091  basellem3  27228  dchrptlem2  27410  bcmono  27422  lgsne0  27480  crctcshwlkn0lem3  30142  fzo0opth  33129  pfxlsw2ccat  33251  wrdt2ind  33254  gsumzrsum  33366  gsummulgc2  33367  gsumwrd2dccatlem  33378  cycpmco2lem7  33433  cyc3conja  33458  archiabllem1b  33493  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem3  33545  elrgspnlem4  33546  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  selvply1rhmlemb  33890  esplyfval0  33935  esplyfval2  33936  esplympl  33938  esplyfval3  33943  vietadeg1  33949  constrrecl  34140  constrimcl  34141  constrmulcl  34142  constrreinvcl  34143  constrinvcl  34144  constrresqrtcl  34148  constrabscl  34149  constrsqrtcl  34150  cos9thpiminplylem1  34153  cos9thpiminplylem2  34154  cos9thpiminply  34159  cos9thpinconstrlem1  34160  oddpwdc  34725  ballotlemfval0  34867  fsum2dsub  34975  breprexplemc  35000  breprexp  35001  circlemeth  35008  fwddifnp1  36638  knoppcnlem6  37068  knoppcnlem9  37071  knoppcn  37074  knoppndvlem2  37083  knoppndvlem4  37085  knoppf  37105  itg2addnclem2  38304  lcmineqlem4  42780  lcmineqlem18  42794  aks4d1p1p2  42818  aks4d1p3  42826  aks4d1p7d1  42830  aks4d1p7  42831  aks4d1p8  42835  aks4d1p9  42836  posbezout  42848  primrootspoweq0  42854  aks6d1c1  42864  aks6d1c2lem4  42875  aks6d1c2  42878  aks6d1c5lem1  42884  aks6d1c5lem2  42886  2np3bcnp1  42892  sticksstones12a  42905  sticksstones22  42916  aks6d1c6lem3  42920  aks6d1c6lem4  42921  aks6d1c6isolem1  42922  aks6d1c6lem5  42925  bcled  42926  bcle2d  42927  aks6d1c7lem1  42928  aks6d1c7lem2  42929  evlselvlem  43303  evlselv  43304  mhphf  43312  fltnltalem  43377  rmynn  43666  jm2.24nn  43669  jm2.17c  43672  jm2.24  43673  acongrep  43690  acongeq  43693  jm2.18  43698  jm2.23  43706  jm2.20nn  43707  jm2.27a  43715  jm2.27c  43717  rmydioph  43724  hashnzfz  45013  bccbc  45038  binomcxplemnn0  45042  binomcxplemrat  45043  binomcxplemnotnn0  45049  mccllem  46296  expfac  46354  0cnv  46439  lmbr3v  46442  sinaover2ne0  46565  dvnmul  46640  dvnprodlem1  46643  dvnprodlem2  46644  stoweidlem11  46708  stoweidlem26  46723  stoweidlem34  46731  stirlinglem5  46775  fourierdlem11  46815  fourierdlem12  46816  fourierdlem14  46818  fourierdlem15  46819  fourierdlem24  46828  fourierdlem25  46829  fourierdlem36  46840  fourierdlem37  46841  fourierdlem41  46845  fourierdlem48  46851  fourierdlem49  46852  fourierdlem50  46853  fourierdlem64  46867  fourierdlem69  46872  fourierdlem73  46876  fourierdlem79  46882  fourierdlem81  46884  fourierdlem92  46895  fourierdlem93  46896  fourierdlem111  46914  elaa2lem  46930  etransclem3  46934  etransclem7  46938  etransclem10  46941  etransclem24  46955  etransclem27  46958  etransclem35  46966  etransclem44  46975  etransclem46  46977  etransclem47  46978  etransclem48  46979  natglobalincr  47576  chnsubseqwl  47578  chnsubseq  47579  2ffzoeq  48048  iccpartigtl  48155  iccpartltu  48157  iccpartgt  48159  0even  48985  2zrngamgm  48993  altgsumbcALT  49116  expnegico01  49281  dig0  49369  nn0sumshdiglem2  49385