Theorem 0zd 12627

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  0cc0 11124  ℤcz 12615

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11182  ax-addrcl 11185  ax-rnegex 11195  ax-cnre 11197

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-neg 11468  df-z 12616

This theorem is used by:  fzctr  13695  fzosubel3  13782  bcval5  14382  snopiswrd  14588  wrdsymb0  14614  ccatsymb  14648  swrdspsleq  14735  pfxnd  14757  pfxccatin12lem1  14797  swrdccat  14804  repswswrd  14855  eqwrds3  15034  fzomaxdiflem  15430  fsumzcl  15821  isumnn0nn  15931  climcndslem1  15938  climcnds  15940  harmonic  15948  geolim  15959  geolim2  15960  geoisum  15966  geoisumr  15967  mertenslem1  15973  mertenslem2  15974  mertens  15975  risefacval2  16097  fallfacval2  16098  binomfallfaclem2  16126  bpolydiflem  16140  eff  16167  efcvg  16171  reefcl  16173  efcj  16178  eftlub  16197  effsumlt  16199  eflegeo  16209  eirrlem  16292  ruclem6  16323  dvdsmodexp  16350  dvdsmod  16419  pwp1fsum  16481  bitsinv1lem  16531  sadcf  16543  sadadd3  16551  smupf  16568  gcdmultipled  16624  alginv  16665  algcvg  16666  algcvga  16669  algfx  16670  eucalgcvga  16676  eucalg  16677  lcmftp  16726  phiprmpw  16867  iserodd  16927  pcpre1  16934  qexpz  16993  prmreclem4  17011  vdwapun  17066  chnpolfz  18721  smndex2dnrinv  19027  odf1  19689  ablsimpgfindlem1  20236  srgbinomlem4  20368  pzriprnglem5  21698  pzriprnglem8  21701  pzriprnglem10  21703  pzriprnglem11  21704  pzriprng1ALT  21709  psrbagres  22145  evlslem1  22298  evlsvvvallem  22307  selvvvval  22358  psdmul  22394  cpmadugsumlemF  23101  dvnff  26150  dgrcl  26459  dgrub  26460  dgrlb  26462  elqaalem2  26552  elqaalem3  26553  geolim3  26575  tayl0  26598  dvtaylp  26606  radcnvlem1  26649  radcnvlem3  26651  radcnv0  26652  radcnvlt2  26655  pserulm  26658  psercn2  26659  pserdvlem2  26664  pserdv2  26666  abelthlem4  26670  abelthlem5  26671  abelthlem6  26672  abelthlem7  26674  abelthlem8  26675  abelthlem9  26676  cos02pilt1  26763  cosne0  26766  logtayl  26897  leibpi  27179  leibpisum  27180  log2cnv  27181  log2tlbnd  27182  basellem3  27319  dchrptlem2  27501  bcmono  27513  lgsne0  27571  crctcshwlkn0lem3  30280  fzo0opth  33274  pfxlsw2ccat  33392  wrdt2ind  33395  gsumzrsum  33505  gsummulgc2  33506  gsumwrd2dccatlem  33517  cycpmco2lem7  33572  cyc3conja  33597  archiabllem1b  33632  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnlem4  33685  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  selvply1rhmlemb  34029  esplyfval0  34074  esplyfval2  34075  esplympl  34077  esplyfval3  34082  vietadeg1  34088  constrrecl  34279  constrimcl  34280  constrmulcl  34281  constrreinvcl  34282  constrinvcl  34283  constrresqrtcl  34287  constrabscl  34288  constrsqrtcl  34289  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminply  34298  cos9thpinconstrlem1  34299  oddpwdc  34865  ballotlemfval0  35007  fsum2dsub  35115  breprexplemc  35140  breprexp  35141  circlemeth  35148  fwddifnp1  36745  knoppcnlem6  37195  knoppcnlem9  37198  knoppcn  37201  knoppndvlem2  37210  knoppndvlem4  37212  knoppf  37232  itg2addnclem2  38421  lcmineqlem4  42898  lcmineqlem18  42912  aks4d1p1p2  42936  aks4d1p3  42944  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  aks4d1p9  42954  posbezout  42966  primrootspoweq0  42972  aks6d1c1  42982  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c5lem1  43002  aks6d1c5lem2  43004  2np3bcnp1  43010  sticksstones12a  43023  sticksstones22  43034  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c6isolem1  43040  aks6d1c6lem5  43043  bcled  43044  bcle2d  43045  aks6d1c7lem1  43046  aks6d1c7lem2  43047  evlselvlem  43434  evlselv  43435  mhphf  43443  fltnltalem  43508  rmynn  43797  jm2.24nn  43800  jm2.17c  43803  jm2.24  43804  acongrep  43821  acongeq  43824  jm2.18  43829  jm2.23  43837  jm2.20nn  43838  jm2.27a  43846  jm2.27c  43848  rmydioph  43855  hashnzfz  45144  bccbc  45169  binomcxplemnn0  45173  binomcxplemrat  45174  binomcxplemnotnn0  45180  mccllem  46427  expfac  46485  0cnv  46570  lmbr3v  46573  sinaover2ne0  46696  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  stoweidlem11  46839  stoweidlem26  46854  stoweidlem34  46862  stirlinglem5  46906  fourierdlem11  46946  fourierdlem12  46947  fourierdlem14  46949  fourierdlem15  46950  fourierdlem24  46959  fourierdlem25  46960  fourierdlem36  46971  fourierdlem37  46972  fourierdlem41  46976  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem64  46998  fourierdlem69  47003  fourierdlem73  47007  fourierdlem79  47013  fourierdlem81  47015  fourierdlem92  47026  fourierdlem93  47027  fourierdlem111  47045  elaa2lem  47061  etransclem3  47065  etransclem7  47069  etransclem10  47072  etransclem24  47086  etransclem27  47089  etransclem35  47097  etransclem44  47106  etransclem46  47108  etransclem47  47109  etransclem48  47110  chnsubseqwl  47707  chnsubseq  47708  2ffzoeq  48216  iccpartigtl  48323  iccpartltu  48325  iccpartgt  48327  0even  49152  2zrngamgm  49160  altgsumbcALT  49283  expnegico01  49448  dig0  49536  nn0sumshdiglem2  49552