Theorem 0zd 12599

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

Syntax hints:   → wi 4   ∈ wcel 2149  0cc0 11096  ℤcz 12587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154  ax-addrcl 11157  ax-rnegex 11167  ax-cnre 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6489  df-fv 6541  df-ov 7411  df-neg 11440  df-z 12588

This theorem is referenced by:  fzctr  13664  fzosubel3  13751  bcval5  14350  snopiswrd  14556  wrdsymb0  14582  ccatsymb  14616  swrdspsleq  14699  pfxnd  14721  pfxccatin12lem1  14761  swrdccat  14768  repswswrd  14817  eqwrds3  14994  fzomaxdiflem  15390  fsumzcl  15782  isumnn0nn  15892  climcndslem1  15899  climcnds  15901  harmonic  15909  geolim  15920  geolim2  15921  geoisum  15927  geoisumr  15928  mertenslem1  15934  mertenslem2  15935  mertens  15936  risefacval2  16060  fallfacval2  16061  binomfallfaclem2  16090  bpolydiflem  16104  eff  16131  efcvg  16135  reefcl  16137  efcj  16142  eftlub  16161  effsumlt  16163  eflegeo  16173  eirrlem  16256  ruclem6  16287  dvdsmodexp  16314  dvdsmod  16383  pwp1fsum  16445  bitsinv1lem  16495  sadcf  16507  sadadd3  16515  smupf  16532  gcdmultipled  16588  alginv  16629  algcvg  16630  algcvga  16633  algfx  16634  eucalgcvga  16640  eucalg  16641  lcmftp  16690  phiprmpw  16831  iserodd  16891  pcpre1  16898  qexpz  16957  prmreclem4  16975  vdwapun  17030  chnpolfz  18685  smndex2dnrinv  18973  odf1  19628  ablsimpgfindlem1  20175  srgbinomlem4  20307  pzriprnglem5  21600  pzriprnglem8  21603  pzriprnglem10  21605  pzriprnglem11  21606  pzriprng1ALT  21611  psrbagres  22045  evlslem1  22198  evlsvvvallem  22207  selvvvval  22258  psdmul  22294  cpmadugsumlemF  22998  dvnff  26047  dgrcl  26355  dgrub  26356  dgrlb  26358  elqaalem2  26446  elqaalem3  26447  geolim3  26465  tayl0  26487  dvtaylp  26495  radcnvlem1  26538  radcnvlem3  26540  radcnv0  26541  radcnvlt2  26544  pserulm  26547  psercn2  26548  pserdvlem2  26553  pserdv2  26555  abelthlem4  26559  abelthlem5  26560  abelthlem6  26561  abelthlem7  26563  abelthlem8  26564  abelthlem9  26565  cos02pilt1  26653  cosne0  26656  logtayl  26787  leibpi  27069  leibpisum  27070  log2cnv  27071  log2tlbnd  27072  basellem3  27209  dchrptlem2  27391  bcmono  27403  lgsne0  27461  crctcshwlkn0lem3  30098  fzo0opth  33085  pfxlsw2ccat  33207  wrdt2ind  33210  gsumzrsum  33322  gsummulgc2  33323  gsumwrd2dccatlem  33334  cycpmco2lem7  33389  cyc3conja  33414  archiabllem1b  33449  elrgspnlem1  33499  elrgspnlem2  33500  elrgspnlem3  33501  elrgspnlem4  33502  elrgspnsubrunlem1  33504  elrgspnsubrunlem2  33505  selvply1rhmlemb  33850  esplyfval0  33895  esplyfval2  33896  esplympl  33898  esplyfval3  33903  vietadeg1  33909  constrrecl  34100  constrimcl  34101  constrmulcl  34102  constrreinvcl  34103  constrinvcl  34104  constrresqrtcl  34108  constrabscl  34109  constrsqrtcl  34110  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  cos9thpiminply  34119  cos9thpinconstrlem1  34120  oddpwdc  34685  ballotlemfval0  34827  fsum2dsub  34935  breprexplemc  34960  breprexp  34961  circlemeth  34968  fwddifnp1  36552  knoppcnlem6  36972  knoppcnlem9  36975  knoppcn  36978  knoppndvlem2  36987  knoppndvlem4  36989  knoppf  37009  itg2addnclem2  38206  lcmineqlem4  42684  lcmineqlem18  42698  aks4d1p1p2  42722  aks4d1p3  42730  aks4d1p7d1  42734  aks4d1p7  42735  aks4d1p8  42739  aks4d1p9  42740  posbezout  42752  primrootspoweq0  42758  aks6d1c1  42768  aks6d1c2lem4  42779  aks6d1c2  42782  aks6d1c5lem1  42788  aks6d1c5lem2  42790  2np3bcnp1  42796  sticksstones12a  42809  sticksstones22  42820  aks6d1c6lem3  42824  aks6d1c6lem4  42825  aks6d1c6isolem1  42826  aks6d1c6lem5  42829  bcled  42830  bcle2d  42831  aks6d1c7lem1  42832  aks6d1c7lem2  42833  evlselvlem  43205  evlselv  43206  mhphf  43214  fltnltalem  43279  rmynn  43568  jm2.24nn  43571  jm2.17c  43574  jm2.24  43575  acongrep  43592  acongeq  43595  jm2.18  43600  jm2.23  43608  jm2.20nn  43609  jm2.27a  43617  jm2.27c  43619  rmydioph  43626  hashnzfz  44915  bccbc  44940  binomcxplemnn0  44944  binomcxplemrat  44945  binomcxplemnotnn0  44951  mccllem  46198  expfac  46256  0cnv  46341  lmbr3v  46344  sinaover2ne0  46467  dvnmul  46542  dvnprodlem1  46545  dvnprodlem2  46546  stoweidlem11  46610  stoweidlem26  46625  stoweidlem34  46633  stirlinglem5  46677  fourierdlem11  46717  fourierdlem12  46718  fourierdlem14  46720  fourierdlem15  46721  fourierdlem24  46730  fourierdlem25  46731  fourierdlem36  46742  fourierdlem37  46743  fourierdlem41  46747  fourierdlem48  46753  fourierdlem49  46754  fourierdlem50  46755  fourierdlem64  46769  fourierdlem69  46774  fourierdlem73  46778  fourierdlem79  46784  fourierdlem81  46786  fourierdlem92  46797  fourierdlem93  46798  fourierdlem111  46816  elaa2lem  46832  etransclem3  46836  etransclem7  46840  etransclem10  46843  etransclem24  46857  etransclem27  46860  etransclem35  46868  etransclem44  46877  etransclem46  46879  etransclem47  46880  etransclem48  46881  natglobalincr  47478  chnsubseqwl  47480  chnsubseq  47481  2ffzoeq  47947  iccpartigtl  48054  iccpartltu  48056  iccpartgt  48058  0even  48884  2zrngamgm  48892  altgsumbcALT  49011  expnegico01  49176  dig0  49264  nn0sumshdiglem2  49280