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

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

Proof of Theorem 0zd
StepHypRef Expression
1 0z 11426 . 2 0 ∈ ℤ
21a1i 11 1 (𝜑 → 0 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  0cc0 9974  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416
This theorem is referenced by:  fzctr  12490  fzosubel3  12568  bcval5  13145  snopiswrd  13346  wrdsymb0  13371  ccatsymb  13400  swrdspsleq  13495  swrdccatin12lem2b  13532  swrdccat  13539  repswswrd  13577  eqwrds3  13750  fzomaxdiflem  14126  fsumzcl  14510  isumnn0nn  14618  climcndslem1  14625  climcnds  14627  harmonic  14635  geolim  14645  geolim2  14646  geoisum  14652  geoisumr  14653  mertenslem1  14660  mertenslem2  14661  mertens  14662  risefacval2  14785  fallfacval2  14786  binomfallfaclem2  14815  bpolydiflem  14829  eff  14856  efcvg  14859  reefcl  14861  efcj  14866  eftlub  14883  effsumlt  14885  eflegeo  14895  eirrlem  14976  ruclem6  15008  dvdsmodexp  15035  dvdsmod  15097  pwp1fsum  15161  bitsinv1lem  15210  sadcf  15222  sadadd3  15230  smupf  15247  alginv  15335  algcvg  15336  algcvga  15339  algfx  15340  eucalgcvga  15346  eucalg  15347  lcmftp  15396  phiprmpw  15528  iserodd  15587  pcpre1  15594  qexpz  15652  prmreclem4  15670  vdwapun  15725  odf1  18025  srgbinomlem4  18589  evlslem1  19563  cpmadugsumlemF  20729  dvnff  23731  dgrcl  24034  dgrub  24035  dgrlb  24037  elqaalem2  24120  elqaalem3  24121  geolim3  24139  tayl0  24161  dvtaylp  24169  radcnvlem1  24212  radcnvlem3  24214  radcnv0  24215  radcnvlt2  24218  pserulm  24221  psercn2  24222  pserdvlem2  24227  pserdv2  24229  abelthlem4  24233  abelthlem5  24234  abelthlem6  24235  abelthlem7  24237  abelthlem8  24238  abelthlem9  24239  cosne0  24321  logtayl  24451  leibpi  24714  leibpisum  24715  log2cnv  24716  log2tlbnd  24717  basellem3  24854  dchrptlem2  25035  bcmono  25047  lgsne0  25105  crctcshwlkn0lem3  26760  archiabllem1b  29874  oddpwdc  30544  ballotlemfval0  30685  fsum2dsub  30813  breprexplemc  30838  breprexp  30839  circlemeth  30846  fwddifnp1  32397  knoppcnlem6  32613  knoppcnlem9  32616  knoppcn  32619  knoppndvlem2  32629  knoppndvlem4  32631  knoppf  32651  itg2addnclem2  33592  rmynn  37840  jm2.24nn  37843  jm2.17c  37846  jm2.24  37847  acongrep  37864  acongeq  37867  jm2.18  37872  jm2.23  37880  jm2.20nn  37881  jm2.27a  37889  jm2.27c  37891  rmydioph  37898  hashnzfz  38836  bccbc  38861  binomcxplemnn0  38865  binomcxplemrat  38866  binomcxplemnotnn0  38872  mccllem  40147  expfac  40207  0cnv  40292  lmbr3v  40295  sinaover2ne0  40397  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  stoweidlem11  40546  stoweidlem26  40561  stoweidlem34  40569  stirlinglem5  40613  fourierdlem11  40653  fourierdlem12  40654  fourierdlem14  40656  fourierdlem15  40657  fourierdlem24  40666  fourierdlem25  40667  fourierdlem36  40678  fourierdlem37  40679  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem64  40705  fourierdlem69  40710  fourierdlem73  40714  fourierdlem79  40720  fourierdlem81  40722  fourierdlem92  40733  fourierdlem93  40734  fourierdlem111  40752  elaa2lem  40768  etransclem3  40772  etransclem7  40776  etransclem10  40779  etransclem24  40793  etransclem27  40796  etransclem35  40804  etransclem44  40813  etransclem46  40815  etransclem47  40816  etransclem48  40817  2ffzoeq  41663  iccpartigtl  41684  iccpartltu  41686  iccpartgt  41688  pfxnd  41720  pfxccatin12lem1  41748  0even  42256  2zrngamgm  42264  altgsumbcALT  42456  expnegico01  42633  dig0  42725  nn0sumshdiglem2  42741
  Copyright terms: Public domain W3C validator