Theorem 0zd 12491

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

Syntax hints:   → wi 4   ∈ wcel 2113  0cc0 11017  ℤcz 12479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11075  ax-addrcl 11078  ax-rnegex 11088  ax-cnre 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-neg 11358  df-z 12480

This theorem is referenced by:  fzctr  13547  fzosubel3  13633  bcval5  14232  snopiswrd  14437  wrdsymb0  14463  ccatsymb  14497  swrdspsleq  14580  pfxnd  14602  pfxccatin12lem1  14642  swrdccat  14649  repswswrd  14698  eqwrds3  14875  fzomaxdiflem  15257  fsumzcl  15649  isumnn0nn  15756  climcndslem1  15763  climcnds  15765  harmonic  15773  geolim  15784  geolim2  15785  geoisum  15791  geoisumr  15792  mertenslem1  15798  mertenslem2  15799  mertens  15800  risefacval2  15924  fallfacval2  15925  binomfallfaclem2  15954  bpolydiflem  15968  eff  15995  efcvg  15999  reefcl  16001  efcj  16006  eftlub  16025  effsumlt  16027  eflegeo  16037  eirrlem  16120  ruclem6  16151  dvdsmodexp  16178  dvdsmod  16247  pwp1fsum  16309  bitsinv1lem  16359  sadcf  16371  sadadd3  16379  smupf  16396  gcdmultipled  16452  alginv  16493  algcvg  16494  algcvga  16497  algfx  16498  eucalgcvga  16504  eucalg  16505  lcmftp  16554  phiprmpw  16694  iserodd  16754  pcpre1  16761  qexpz  16820  prmreclem4  16838  vdwapun  16893  chnpolfz  18547  smndex2dnrinv  18831  odf1  19482  ablsimpgfindlem1  20029  srgbinomlem4  20155  pzriprnglem5  21431  pzriprnglem8  21434  pzriprnglem10  21436  pzriprnglem11  21437  pzriprng1ALT  21442  evlslem1  22028  evlsvvvallem  22037  psdmul  22100  cpmadugsumlemF  22811  dvnff  25872  dgrcl  26185  dgrub  26186  dgrlb  26188  elqaalem2  26275  elqaalem3  26276  geolim3  26294  tayl0  26316  dvtaylp  26325  radcnvlem1  26369  radcnvlem3  26371  radcnv0  26372  radcnvlt2  26375  pserulm  26378  psercn2  26379  psercn2OLD  26380  pserdvlem2  26385  pserdv2  26387  abelthlem4  26391  abelthlem5  26392  abelthlem6  26393  abelthlem7  26395  abelthlem8  26396  abelthlem9  26397  cos02pilt1  26482  cosne0  26485  logtayl  26616  leibpi  26899  leibpisum  26900  log2cnv  26901  log2tlbnd  26902  basellem3  27040  dchrptlem2  27223  bcmono  27235  lgsne0  27293  crctcshwlkn0lem3  29811  fzo0opth  32811  pfxlsw2ccat  32960  wrdt2ind  32963  gsumzrsum  33076  gsummulgc2  33077  gsumwrd2dccatlem  33087  cycpmco2lem7  33142  cyc3conja  33167  archiabllem1b  33202  elrgspnlem1  33252  elrgspnlem2  33253  elrgspnlem3  33254  elrgspnlem4  33255  elrgspnsubrunlem1  33257  elrgspnsubrunlem2  33258  esplyfval0  33650  esplyfval2  33651  esplympl  33653  esplyfval3  33658  vietadeg1  33662  constrrecl  33854  constrimcl  33855  constrmulcl  33856  constrreinvcl  33857  constrinvcl  33858  constrresqrtcl  33862  constrabscl  33863  constrsqrtcl  33864  cos9thpiminplylem1  33867  cos9thpiminplylem2  33868  cos9thpiminply  33873  cos9thpinconstrlem1  33874  oddpwdc  34439  ballotlemfval0  34581  fsum2dsub  34692  breprexplemc  34717  breprexp  34718  circlemeth  34725  fwddifnp1  36281  knoppcnlem6  36614  knoppcnlem9  36617  knoppcn  36620  knoppndvlem2  36629  knoppndvlem4  36631  knoppf  36651  itg2addnclem2  37785  lcmineqlem4  42198  lcmineqlem18  42212  aks4d1p1p2  42236  aks4d1p3  42244  aks4d1p7d1  42248  aks4d1p7  42249  aks4d1p8  42253  aks4d1p9  42254  posbezout  42266  primrootspoweq0  42272  aks6d1c1  42282  aks6d1c2lem4  42293  aks6d1c2  42296  aks6d1c5lem1  42302  aks6d1c5lem2  42304  2np3bcnp1  42310  sticksstones12a  42323  sticksstones22  42334  aks6d1c6lem3  42338  aks6d1c6lem4  42339  aks6d1c6isolem1  42340  aks6d1c6lem5  42343  bcled  42344  bcle2d  42345  aks6d1c7lem1  42346  aks6d1c7lem2  42347  psrbagres  42714  selvvvval  42743  evlselvlem  42744  evlselv  42745  mhphf  42755  fltnltalem  42820  rmynn  43113  jm2.24nn  43116  jm2.17c  43119  jm2.24  43120  acongrep  43137  acongeq  43140  jm2.18  43145  jm2.23  43153  jm2.20nn  43154  jm2.27a  43162  jm2.27c  43164  rmydioph  43171  hashnzfz  44477  bccbc  44502  binomcxplemnn0  44506  binomcxplemrat  44507  binomcxplemnotnn0  44513  mccllem  45759  expfac  45817  0cnv  45902  lmbr3v  45905  sinaover2ne0  46028  dvnmul  46103  dvnprodlem1  46106  dvnprodlem2  46107  stoweidlem11  46171  stoweidlem26  46186  stoweidlem34  46194  stirlinglem5  46238  fourierdlem11  46278  fourierdlem12  46279  fourierdlem14  46281  fourierdlem15  46282  fourierdlem24  46291  fourierdlem25  46292  fourierdlem36  46303  fourierdlem37  46304  fourierdlem41  46308  fourierdlem48  46314  fourierdlem49  46315  fourierdlem50  46316  fourierdlem64  46330  fourierdlem69  46335  fourierdlem73  46339  fourierdlem79  46345  fourierdlem81  46347  fourierdlem92  46358  fourierdlem93  46359  fourierdlem111  46377  elaa2lem  46393  etransclem3  46397  etransclem7  46401  etransclem10  46404  etransclem24  46418  etransclem27  46421  etransclem35  46429  etransclem44  46438  etransclem46  46440  etransclem47  46441  etransclem48  46442  natglobalincr  47037  chnsubseqwl  47039  chnsubseq  47040  2ffzoeq  47489  iccpartigtl  47585  iccpartltu  47587  iccpartgt  47589  0even  48399  2zrngamgm  48407  altgsumbcALT  48515  expnegico01  48680  dig0  48768  nn0sumshdiglem2  48784