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

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

Proof of Theorem 0zd
StepHypRef Expression
1 0z 12517 . 2 0 ∈ ℤ
21a1i 11 1 (𝜑 → 0 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  0cc0 11058  cz 12506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11116  ax-addrcl 11119  ax-rnegex 11129  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-neg 11395  df-z 12507
This theorem is referenced by:  fzctr  13560  fzosubel3  13640  bcval5  14225  snopiswrd  14418  wrdsymb0  14444  ccatsymb  14477  swrdspsleq  14560  pfxnd  14582  pfxccatin12lem1  14623  swrdccat  14630  repswswrd  14679  eqwrds3  14857  fzomaxdiflem  15234  fsumzcl  15627  isumnn0nn  15734  climcndslem1  15741  climcnds  15743  harmonic  15751  geolim  15762  geolim2  15763  geoisum  15769  geoisumr  15770  mertenslem1  15776  mertenslem2  15777  mertens  15778  risefacval2  15900  fallfacval2  15901  binomfallfaclem2  15930  bpolydiflem  15944  eff  15971  efcvg  15974  reefcl  15976  efcj  15981  eftlub  15998  effsumlt  16000  eflegeo  16010  eirrlem  16093  ruclem6  16124  dvdsmodexp  16151  dvdsmod  16218  pwp1fsum  16280  bitsinv1lem  16328  sadcf  16340  sadadd3  16348  smupf  16365  gcdmultipled  16422  alginv  16458  algcvg  16459  algcvga  16462  algfx  16463  eucalgcvga  16469  eucalg  16470  lcmftp  16519  phiprmpw  16655  iserodd  16714  pcpre1  16721  qexpz  16780  prmreclem4  16798  vdwapun  16853  smndex2dnrinv  18732  odf1  19351  ablsimpgfindlem1  19893  srgbinomlem4  19967  evlslem1  21508  cpmadugsumlemF  22241  dvnff  25303  dgrcl  25610  dgrub  25611  dgrlb  25613  elqaalem2  25696  elqaalem3  25697  geolim3  25715  tayl0  25737  dvtaylp  25745  radcnvlem1  25788  radcnvlem3  25790  radcnv0  25791  radcnvlt2  25794  pserulm  25797  psercn2  25798  pserdvlem2  25803  pserdv2  25805  abelthlem4  25809  abelthlem5  25810  abelthlem6  25811  abelthlem7  25813  abelthlem8  25814  abelthlem9  25815  cos02pilt1  25898  cosne0  25901  logtayl  26031  leibpi  26308  leibpisum  26309  log2cnv  26310  log2tlbnd  26311  basellem3  26448  dchrptlem2  26629  bcmono  26641  lgsne0  26699  crctcshwlkn0lem3  28799  pfxlsw2ccat  31848  wrdt2ind  31849  cycpmco2lem7  32023  cyc3conja  32048  archiabllem1b  32070  oddpwdc  32994  ballotlemfval0  33135  fsum2dsub  33260  breprexplemc  33285  breprexp  33286  circlemeth  33293  fwddifnp1  34779  knoppcnlem6  34990  knoppcnlem9  34993  knoppcn  34996  knoppndvlem2  35005  knoppndvlem4  35007  knoppf  35027  itg2addnclem2  36159  lcmineqlem4  40518  lcmineqlem18  40532  aks4d1p1p2  40556  aks4d1p3  40564  aks4d1p7d1  40568  aks4d1p7  40569  aks4d1p8  40573  aks4d1p9  40574  2np3bcnp1  40581  sticksstones12a  40594  sticksstones22  40605  metakunt29  40634  metakunt30  40635  metakunt32  40637  metakunt33  40638  fltnltalem  41029  rmynn  41309  jm2.24nn  41312  jm2.17c  41315  jm2.24  41316  acongrep  41333  acongeq  41336  jm2.18  41341  jm2.23  41349  jm2.20nn  41350  jm2.27a  41358  jm2.27c  41360  rmydioph  41367  hashnzfz  42674  bccbc  42699  binomcxplemnn0  42703  binomcxplemrat  42704  binomcxplemnotnn0  42710  mccllem  43912  expfac  43972  0cnv  44057  lmbr3v  44060  sinaover2ne0  44183  dvnmul  44258  dvnprodlem1  44261  dvnprodlem2  44262  stoweidlem11  44326  stoweidlem26  44341  stoweidlem34  44349  stirlinglem5  44393  fourierdlem11  44433  fourierdlem12  44434  fourierdlem14  44436  fourierdlem15  44437  fourierdlem24  44446  fourierdlem25  44447  fourierdlem36  44458  fourierdlem37  44459  fourierdlem41  44463  fourierdlem48  44469  fourierdlem49  44470  fourierdlem50  44471  fourierdlem64  44485  fourierdlem69  44490  fourierdlem73  44494  fourierdlem79  44500  fourierdlem81  44502  fourierdlem92  44513  fourierdlem93  44514  fourierdlem111  44532  elaa2lem  44548  etransclem3  44552  etransclem7  44556  etransclem10  44559  etransclem24  44573  etransclem27  44576  etransclem35  44584  etransclem44  44593  etransclem46  44595  etransclem47  44596  etransclem48  44597  natglobalincr  45190  2ffzoeq  45634  iccpartigtl  45689  iccpartltu  45691  iccpartgt  45693  0even  46303  2zrngamgm  46311  altgsumbcALT  46503  expnegico01  46673  dig0  46766  nn0sumshdiglem2  46782
  Copyright terms: Public domain W3C validator