Theorem 0zd 12570

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

Syntax hints:   → wi 4   ∈ wcel 2107  0cc0 11110  ℤcz 12558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addrcl 11171  ax-rnegex 11181  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447  df-z 12559

This theorem is referenced by:  fzctr  13613  fzosubel3  13693  bcval5  14278  snopiswrd  14473  wrdsymb0  14499  ccatsymb  14532  swrdspsleq  14615  pfxnd  14637  pfxccatin12lem1  14678  swrdccat  14685  repswswrd  14734  eqwrds3  14912  fzomaxdiflem  15289  fsumzcl  15681  isumnn0nn  15788  climcndslem1  15795  climcnds  15797  harmonic  15805  geolim  15816  geolim2  15817  geoisum  15823  geoisumr  15824  mertenslem1  15830  mertenslem2  15831  mertens  15832  risefacval2  15954  fallfacval2  15955  binomfallfaclem2  15984  bpolydiflem  15998  eff  16025  efcvg  16028  reefcl  16030  efcj  16035  eftlub  16052  effsumlt  16054  eflegeo  16064  eirrlem  16147  ruclem6  16178  dvdsmodexp  16205  dvdsmod  16272  pwp1fsum  16334  bitsinv1lem  16382  sadcf  16394  sadadd3  16402  smupf  16419  gcdmultipled  16476  alginv  16512  algcvg  16513  algcvga  16516  algfx  16517  eucalgcvga  16523  eucalg  16524  lcmftp  16573  phiprmpw  16709  iserodd  16768  pcpre1  16775  qexpz  16834  prmreclem4  16852  vdwapun  16907  smndex2dnrinv  18796  odf1  19430  ablsimpgfindlem1  19977  srgbinomlem4  20052  evlslem1  21645  cpmadugsumlemF  22378  dvnff  25440  dgrcl  25747  dgrub  25748  dgrlb  25750  elqaalem2  25833  elqaalem3  25834  geolim3  25852  tayl0  25874  dvtaylp  25882  radcnvlem1  25925  radcnvlem3  25927  radcnv0  25928  radcnvlt2  25931  pserulm  25934  psercn2  25935  pserdvlem2  25940  pserdv2  25942  abelthlem4  25946  abelthlem5  25947  abelthlem6  25948  abelthlem7  25950  abelthlem8  25951  abelthlem9  25952  cos02pilt1  26035  cosne0  26038  logtayl  26168  leibpi  26447  leibpisum  26448  log2cnv  26449  log2tlbnd  26450  basellem3  26587  dchrptlem2  26768  bcmono  26780  lgsne0  26838  crctcshwlkn0lem3  29066  pfxlsw2ccat  32116  wrdt2ind  32117  cycpmco2lem7  32291  cyc3conja  32316  archiabllem1b  32338  oddpwdc  33353  ballotlemfval0  33494  fsum2dsub  33619  breprexplemc  33644  breprexp  33645  circlemeth  33652  fwddifnp1  35137  gg-psercn2  35178  knoppcnlem6  35374  knoppcnlem9  35377  knoppcn  35380  knoppndvlem2  35389  knoppndvlem4  35391  knoppf  35411  itg2addnclem2  36540  lcmineqlem4  40897  lcmineqlem18  40911  aks4d1p1p2  40935  aks4d1p3  40943  aks4d1p7d1  40947  aks4d1p7  40948  aks4d1p8  40952  aks4d1p9  40953  2np3bcnp1  40960  sticksstones12a  40973  sticksstones22  40984  metakunt29  41013  metakunt30  41014  metakunt32  41016  metakunt33  41017  psrbagres  41115  evlsvvvallem  41133  selvvvval  41157  evlselvlem  41158  evlselv  41159  mhphf  41169  fltnltalem  41404  rmynn  41695  jm2.24nn  41698  jm2.17c  41701  jm2.24  41702  acongrep  41719  acongeq  41722  jm2.18  41727  jm2.23  41735  jm2.20nn  41736  jm2.27a  41744  jm2.27c  41746  rmydioph  41753  hashnzfz  43079  bccbc  43104  binomcxplemnn0  43108  binomcxplemrat  43109  binomcxplemnotnn0  43115  mccllem  44313  expfac  44373  0cnv  44458  lmbr3v  44461  sinaover2ne0  44584  dvnmul  44659  dvnprodlem1  44662  dvnprodlem2  44663  stoweidlem11  44727  stoweidlem26  44742  stoweidlem34  44750  stirlinglem5  44794  fourierdlem11  44834  fourierdlem12  44835  fourierdlem14  44837  fourierdlem15  44838  fourierdlem24  44847  fourierdlem25  44848  fourierdlem36  44859  fourierdlem37  44860  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem64  44886  fourierdlem69  44891  fourierdlem73  44895  fourierdlem79  44901  fourierdlem81  44903  fourierdlem92  44914  fourierdlem93  44915  fourierdlem111  44933  elaa2lem  44949  etransclem3  44953  etransclem7  44957  etransclem10  44960  etransclem24  44974  etransclem27  44977  etransclem35  44985  etransclem44  44994  etransclem46  44996  etransclem47  44997  etransclem48  44998  natglobalincr  45591  2ffzoeq  46036  iccpartigtl  46091  iccpartltu  46093  iccpartgt  46095  pzriprnglem5  46809  pzriprnglem8  46812  pzriprnglem10  46814  pzriprnglem11  46815  pzriprng1ALT  46820  0even  46829  2zrngamgm  46837  altgsumbcALT  47029  expnegico01  47199  dig0  47292  nn0sumshdiglem2  47308