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

Theorem 0zd 11601
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 11600 . 2 0 ∈ ℤ
21a1i 11 1 (𝜑 → 0 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  0cc0 10148  cz 11589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-i2m1 10216  ax-1ne0 10217  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-neg 10481  df-z 11590
This theorem is referenced by:  fzctr  12665  fzosubel3  12743  bcval5  13319  snopiswrd  13520  wrdsymb0  13545  ccatsymb  13574  swrdspsleq  13669  swrdccatin12lem2b  13706  swrdccat  13713  repswswrd  13751  eqwrds3  13925  fzomaxdiflem  14301  fsumzcl  14685  isumnn0nn  14793  climcndslem1  14800  climcnds  14802  harmonic  14810  geolim  14820  geolim2  14821  geoisum  14827  geoisumr  14828  mertenslem1  14835  mertenslem2  14836  mertens  14837  risefacval2  14960  fallfacval2  14961  binomfallfaclem2  14990  bpolydiflem  15004  eff  15031  efcvg  15034  reefcl  15036  efcj  15041  eftlub  15058  effsumlt  15060  eflegeo  15070  eirrlem  15151  ruclem6  15183  dvdsmodexp  15210  dvdsmod  15272  pwp1fsum  15336  bitsinv1lem  15385  sadcf  15397  sadadd3  15405  smupf  15422  alginv  15510  algcvg  15511  algcvga  15514  algfx  15515  eucalgcvga  15521  eucalg  15522  lcmftp  15571  phiprmpw  15703  iserodd  15762  pcpre1  15769  qexpz  15827  prmreclem4  15845  vdwapun  15900  odf1  18199  srgbinomlem4  18763  evlslem1  19737  cpmadugsumlemF  20903  dvnff  23905  dgrcl  24208  dgrub  24209  dgrlb  24211  elqaalem2  24294  elqaalem3  24295  geolim3  24313  tayl0  24335  dvtaylp  24343  radcnvlem1  24386  radcnvlem3  24388  radcnv0  24389  radcnvlt2  24392  pserulm  24395  psercn2  24396  pserdvlem2  24401  pserdv2  24403  abelthlem4  24407  abelthlem5  24408  abelthlem6  24409  abelthlem7  24411  abelthlem8  24412  abelthlem9  24413  cosne0  24496  logtayl  24626  leibpi  24889  leibpisum  24890  log2cnv  24891  log2tlbnd  24892  basellem3  25029  dchrptlem2  25210  bcmono  25222  lgsne0  25280  crctcshwlkn0lem3  26936  archiabllem1b  30076  oddpwdc  30746  ballotlemfval0  30887  fsum2dsub  31015  breprexplemc  31040  breprexp  31041  circlemeth  31048  fwddifnp1  32599  knoppcnlem6  32815  knoppcnlem9  32818  knoppcn  32821  knoppndvlem2  32831  knoppndvlem4  32833  knoppf  32853  itg2addnclem2  33793  rmynn  38043  jm2.24nn  38046  jm2.17c  38049  jm2.24  38050  acongrep  38067  acongeq  38070  jm2.18  38075  jm2.23  38083  jm2.20nn  38084  jm2.27a  38092  jm2.27c  38094  rmydioph  38101  hashnzfz  39039  bccbc  39064  binomcxplemnn0  39068  binomcxplemrat  39069  binomcxplemnotnn0  39075  mccllem  40350  expfac  40410  0cnv  40495  lmbr3v  40498  sinaover2ne0  40600  dvnmul  40679  dvnprodlem1  40682  dvnprodlem2  40683  stoweidlem11  40749  stoweidlem26  40764  stoweidlem34  40772  stirlinglem5  40816  fourierdlem11  40856  fourierdlem12  40857  fourierdlem14  40859  fourierdlem15  40860  fourierdlem24  40869  fourierdlem25  40870  fourierdlem36  40881  fourierdlem37  40882  fourierdlem41  40886  fourierdlem48  40892  fourierdlem49  40893  fourierdlem50  40894  fourierdlem64  40908  fourierdlem69  40913  fourierdlem73  40917  fourierdlem79  40923  fourierdlem81  40925  fourierdlem92  40936  fourierdlem93  40937  fourierdlem111  40955  elaa2lem  40971  etransclem3  40975  etransclem7  40979  etransclem10  40982  etransclem24  40996  etransclem27  40999  etransclem35  41007  etransclem44  41016  etransclem46  41018  etransclem47  41019  etransclem48  41020  2ffzoeq  41866  iccpartigtl  41887  iccpartltu  41889  iccpartgt  41891  pfxnd  41923  pfxccatin12lem1  41951  0even  42459  2zrngamgm  42467  altgsumbcALT  42659  expnegico01  42836  dig0  42928  nn0sumshdiglem2  42944
  Copyright terms: Public domain W3C validator