Theorem 0zd 12045

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

Syntax hints:   → wi 4   ∈ wcel 2111  0cc0 10588  ℤcz 12033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-1cn 10646  ax-addrcl 10649  ax-rnegex 10659  ax-cnre 10661

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-iota 6299  df-fv 6348  df-ov 7159  df-neg 10924  df-z 12034

This theorem is referenced by:  fzctr  13081  fzosubel3  13160  bcval5  13741  snopiswrd  13935  wrdsymb0  13961  ccatsymb  13996  swrdspsleq  14087  pfxnd  14109  pfxccatin12lem1  14150  swrdccat  14157  repswswrd  14206  eqwrds3  14385  fzomaxdiflem  14763  fsumzcl  15153  isumnn0nn  15258  climcndslem1  15265  climcnds  15267  harmonic  15275  geolim  15287  geolim2  15288  geoisum  15294  geoisumr  15295  mertenslem1  15301  mertenslem2  15302  mertens  15303  risefacval2  15425  fallfacval2  15426  binomfallfaclem2  15455  bpolydiflem  15469  eff  15496  efcvg  15499  reefcl  15501  efcj  15506  eftlub  15523  effsumlt  15525  eflegeo  15535  eirrlem  15618  ruclem6  15649  dvdsmodexp  15676  dvdsmod  15743  pwp1fsum  15805  bitsinv1lem  15853  sadcf  15865  sadadd3  15873  smupf  15890  gcdmultipled  15947  alginv  15985  algcvg  15986  algcvga  15989  algfx  15990  eucalgcvga  15996  eucalg  15997  lcmftp  16046  phiprmpw  16182  iserodd  16241  pcpre1  16248  qexpz  16306  prmreclem4  16324  vdwapun  16379  smndex2dnrinv  18160  odf1  18770  ablsimpgfindlem1  19311  srgbinomlem4  19375  evlslem1  20859  cpmadugsumlemF  21590  dvnff  24636  dgrcl  24943  dgrub  24944  dgrlb  24946  elqaalem2  25029  elqaalem3  25030  geolim3  25048  tayl0  25070  dvtaylp  25078  radcnvlem1  25121  radcnvlem3  25123  radcnv0  25124  radcnvlt2  25127  pserulm  25130  psercn2  25131  pserdvlem2  25136  pserdv2  25138  abelthlem4  25142  abelthlem5  25143  abelthlem6  25144  abelthlem7  25146  abelthlem8  25147  abelthlem9  25148  cos02pilt1  25231  cosne0  25234  logtayl  25364  leibpi  25641  leibpisum  25642  log2cnv  25643  log2tlbnd  25644  basellem3  25781  dchrptlem2  25962  bcmono  25974  lgsne0  26032  crctcshwlkn0lem3  27711  pfxlsw2ccat  30761  wrdt2ind  30762  cycpmco2lem7  30938  cyc3conja  30963  archiabllem1b  30985  oddpwdc  31853  ballotlemfval0  31994  fsum2dsub  32119  breprexplemc  32144  breprexp  32145  circlemeth  32152  fwddifnp1  34051  knoppcnlem6  34262  knoppcnlem9  34265  knoppcn  34268  knoppndvlem2  34277  knoppndvlem4  34279  knoppf  34299  itg2addnclem2  35424  lcmineqlem4  39634  lcmineqlem18  39648  aks4d1p1p2  39671  2np3bcnp1  39680  metakunt29  39710  metakunt30  39711  metakunt32  39713  metakunt33  39714  fltnltalem  40036  rmynn  40315  jm2.24nn  40318  jm2.17c  40321  jm2.24  40322  acongrep  40339  acongeq  40342  jm2.18  40347  jm2.23  40355  jm2.20nn  40356  jm2.27a  40364  jm2.27c  40366  rmydioph  40373  hashnzfz  41442  bccbc  41467  binomcxplemnn0  41471  binomcxplemrat  41472  binomcxplemnotnn0  41478  mccllem  42650  expfac  42710  0cnv  42795  lmbr3v  42798  sinaover2ne0  42921  dvnmul  42996  dvnprodlem1  42999  dvnprodlem2  43000  stoweidlem11  43064  stoweidlem26  43079  stoweidlem34  43087  stirlinglem5  43131  fourierdlem11  43171  fourierdlem12  43172  fourierdlem14  43174  fourierdlem15  43175  fourierdlem24  43184  fourierdlem25  43185  fourierdlem36  43196  fourierdlem37  43197  fourierdlem41  43201  fourierdlem48  43207  fourierdlem49  43208  fourierdlem50  43209  fourierdlem64  43223  fourierdlem69  43228  fourierdlem73  43232  fourierdlem79  43238  fourierdlem81  43240  fourierdlem92  43251  fourierdlem93  43252  fourierdlem111  43270  elaa2lem  43286  etransclem3  43290  etransclem7  43294  etransclem10  43297  etransclem24  43311  etransclem27  43314  etransclem35  43322  etransclem44  43331  etransclem46  43333  etransclem47  43334  etransclem48  43335  2ffzoeq  44312  iccpartigtl  44367  iccpartltu  44369  iccpartgt  44371  0even  44981  2zrngamgm  44989  altgsumbcALT  45181  expnegico01  45351  dig0  45444  nn0sumshdiglem2  45460