Theorem 0zd 11846

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

Syntax hints:   → wi 4   ∈ wcel 2081  0cc0 10388  ℤcz 11834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-1cn 10446  ax-addrcl 10449  ax-rnegex 10459  ax-cnre 10461

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-iota 6194  df-fv 6238  df-ov 7024  df-neg 10725  df-z 11835

This theorem is referenced by:  fzctr  12874  fzosubel3  12953  bcval5  13533  snopiswrd  13721  wrdsymb0  13752  ccatsymb  13785  swrdspsleq  13868  pfxnd  13890  pfxccatin12lem1  13931  swrdccat  13938  repswswrd  13987  eqwrds3  14164  fzomaxdiflem  14541  fsumzcl  14930  isumnn0nn  15035  climcndslem1  15042  climcnds  15044  harmonic  15052  geolim  15064  geolim2  15065  geoisum  15071  geoisumr  15072  mertenslem1  15078  mertenslem2  15079  mertens  15080  risefacval2  15202  fallfacval2  15203  binomfallfaclem2  15232  bpolydiflem  15246  eff  15273  efcvg  15276  reefcl  15278  efcj  15283  eftlub  15300  effsumlt  15302  eflegeo  15312  eirrlem  15395  ruclem6  15426  dvdsmodexp  15453  dvdsmod  15516  pwp1fsum  15580  bitsinv1lem  15628  sadcf  15640  sadadd3  15648  smupf  15665  alginv  15753  algcvg  15754  algcvga  15757  algfx  15758  eucalgcvga  15764  eucalg  15765  lcmftp  15814  phiprmpw  15947  iserodd  16006  pcpre1  16013  qexpz  16071  prmreclem4  16089  vdwapun  16144  odf1  18424  srgbinomlem4  18988  evlslem1  19987  cpmadugsumlemF  21173  dvnff  24208  dgrcl  24511  dgrub  24512  dgrlb  24514  elqaalem2  24597  elqaalem3  24598  geolim3  24616  tayl0  24638  dvtaylp  24646  radcnvlem1  24689  radcnvlem3  24691  radcnv0  24692  radcnvlt2  24695  pserulm  24698  psercn2  24699  pserdvlem2  24704  pserdv2  24706  abelthlem4  24710  abelthlem5  24711  abelthlem6  24712  abelthlem7  24714  abelthlem8  24715  abelthlem9  24716  cosne0  24800  logtayl  24929  leibpi  25207  leibpisum  25208  log2cnv  25209  log2tlbnd  25210  basellem3  25347  dchrptlem2  25528  bcmono  25540  lgsne0  25598  crctcshwlkn0lem3  27282  pfxlsw2ccat  30310  wrdt2ind  30311  cyc3conja  30442  archiabllem1b  30464  oddpwdc  31234  ballotlemfval0  31375  fsum2dsub  31500  breprexplemc  31525  breprexp  31526  circlemeth  31533  fwddifnp1  33241  knoppcnlem6  33452  knoppcnlem9  33455  knoppcn  33458  knoppndvlem2  33467  knoppndvlem4  33469  knoppf  33489  itg2addnclem2  34500  fltnltalem  38796  rmynn  39063  jm2.24nn  39066  jm2.17c  39069  jm2.24  39070  acongrep  39087  acongeq  39090  jm2.18  39095  jm2.23  39103  jm2.20nn  39104  jm2.27a  39112  jm2.27c  39114  rmydioph  39121  gcdmuld  40083  ablsimpgfindlem1  40190  hashnzfz  40215  bccbc  40240  binomcxplemnn0  40244  binomcxplemrat  40245  binomcxplemnotnn0  40251  mccllem  41445  expfac  41505  0cnv  41590  lmbr3v  41593  sinaover2ne0  41716  dvnmul  41795  dvnprodlem1  41798  dvnprodlem2  41799  stoweidlem11  41864  stoweidlem26  41879  stoweidlem34  41887  stirlinglem5  41931  fourierdlem11  41971  fourierdlem12  41972  fourierdlem14  41974  fourierdlem15  41975  fourierdlem24  41984  fourierdlem25  41985  fourierdlem36  41996  fourierdlem37  41997  fourierdlem41  42001  fourierdlem48  42007  fourierdlem49  42008  fourierdlem50  42009  fourierdlem64  42023  fourierdlem69  42028  fourierdlem73  42032  fourierdlem79  42038  fourierdlem81  42040  fourierdlem92  42051  fourierdlem93  42052  fourierdlem111  42070  elaa2lem  42086  etransclem3  42090  etransclem7  42094  etransclem10  42097  etransclem24  42111  etransclem27  42114  etransclem35  42122  etransclem44  42131  etransclem46  42133  etransclem47  42134  etransclem48  42135  2ffzoeq  43070  iccpartigtl  43091  iccpartltu  43093  iccpartgt  43095  0even  43706  2zrngamgm  43714  altgsumbcALT  43905  expnegico01  44080  dig0  44173  nn0sumshdiglem2  44189