MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0zd Structured version   Visualization version   GIF version

Theorem 0zd 11225
Description: Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
0zd (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd
StepHypRef Expression
1 0z 11224 . 2 0 ∈ ℤ
21a1i 11 1 (𝜑 → 0 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  0cc0 9793  cz 11213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-i2m1 9861  ax-1ne0 9862  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-neg 10121  df-z 11214
This theorem is referenced by:  fzctr  12278  fzosubel3  12354  bcval5  12925  snopiswrd  13118  wrdsymb0  13143  ccatsymb  13168  swrdspsleq  13250  swrdccatin12lem2b  13286  swrdccat  13293  repswswrd  13331  eqwrds3  13501  fzomaxdiflem  13879  fsumzcl  14262  isumnn0nn  14362  climcndslem1  14369  climcnds  14371  harmonic  14379  geolim  14389  geolim2  14390  geoisum  14396  geoisumr  14397  mertenslem1  14404  mertenslem2  14405  mertens  14406  risefacval2  14529  fallfacval2  14530  binomfallfaclem2  14559  bpolydiflem  14573  eff  14600  efcvg  14603  reefcl  14605  efcj  14610  eftlub  14627  effsumlt  14629  eflegeo  14639  eirrlem  14720  ruclem6  14752  dvdsmod  14837  pwp1fsum  14901  bitsinv1lem  14950  sadcf  14962  sadadd3  14970  smupf  14987  alginv  15075  algcvg  15076  algcvga  15079  algfx  15080  eucalgcvga  15086  eucalg  15087  lcmftp  15136  phiprmpw  15268  fermltl  15276  iserodd  15327  pcpre1  15334  qexpz  15392  prmreclem4  15410  vdwapun  15465  odf1  17751  srgbinomlem4  18315  evlslem1  19285  cpmadugsumlemF  20448  dvnff  23437  dgrcl  23738  dgrub  23739  dgrlb  23741  elqaalem2  23824  elqaalem3  23825  geolim3  23843  tayl0  23865  dvtaylp  23873  radcnvlem1  23916  radcnvlem3  23918  radcnv0  23919  radcnvlt2  23922  pserulm  23925  psercn2  23926  pserdvlem2  23931  pserdv2  23933  abelthlem4  23937  abelthlem5  23938  abelthlem6  23939  abelthlem7  23941  abelthlem8  23942  abelthlem9  23943  cosne0  24025  logtayl  24151  leibpi  24414  leibpisum  24415  log2cnv  24416  log2tlbnd  24417  basellem3  24554  dchrptlem2  24735  bcmono  24747  lgslem4  24770  lgsne0  24805  numclwwlkovf2ex  26407  archiabllem1b  28911  oddpwdc  29577  ballotlemfval0  29718  fwddifnp1  31276  knoppcnlem6  31492  knoppcnlem9  31495  knoppcn  31498  knoppndvlem2  31508  knoppndvlem4  31510  knoppf  31530  itg2addnclem2  32456  rmynn  36365  jm2.24nn  36368  jm2.17c  36371  jm2.24  36372  acongrep  36389  acongeq  36392  jm2.18  36397  jm2.23  36405  jm2.20nn  36406  jm2.27a  36414  jm2.27c  36416  rmydioph  36423  hashnzfz  37365  bccbc  37390  binomcxplemnn0  37394  binomcxplemrat  37395  binomcxplemnotnn0  37401  mccllem  38488  expfac  38548  sinaover2ne0  38575  dvnmul  38657  dvnprodlem1  38660  dvnprodlem2  38661  stoweidlem11  38728  stoweidlem26  38743  stoweidlem34  38751  stirlinglem5  38795  fourierdlem11  38835  fourierdlem12  38836  fourierdlem14  38838  fourierdlem15  38839  fourierdlem24  38848  fourierdlem25  38849  fourierdlem36  38860  fourierdlem37  38861  fourierdlem41  38865  fourierdlem48  38871  fourierdlem49  38872  fourierdlem50  38873  fourierdlem64  38887  fourierdlem69  38892  fourierdlem73  38896  fourierdlem79  38902  fourierdlem81  38904  fourierdlem92  38915  fourierdlem93  38916  fourierdlem111  38934  elaa2lem  38950  etransclem3  38954  etransclem7  38958  etransclem10  38961  etransclem24  38975  etransclem27  38978  etransclem35  38986  etransclem44  38995  etransclem46  38997  etransclem47  38998  etransclem48  38999  iccpartigtl  39786  iccpartltu  39788  iccpartgt  39790  pfxnd  40083  pfxccatin12lem1  40111  2ffzoeq  40208  crctcsh1wlkn0lem3  41037  wwlksnextproplem1  41137  av-numclwwlkovf2ex  41539  0even  41743  2zrngamgm  41751  altgsumbcALT  41946  expnegico01  42124  dig0  42220  nn0sumshdiglem2  42236
  Copyright terms: Public domain W3C validator