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

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

Proof of Theorem 0zd
StepHypRef Expression
1 0z 10900 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  0cc0 9513   cz 10889
This theorem is referenced by:  fzctr  11816  fzosubel3  11877  bcval5  12396  ccatsymb  12600  ccat2s1fvw  12642  swrdspsleq  12673  swrdccatin12lem2b  12711  swrdccat  12718  repswswrd  12756  fzomaxdiflem  13175  fsumzcl  13557  isumnn0nn  13654  climcndslem1  13661  climcnds  13663  harmonic  13670  geolim  13679  geolim2  13680  geoisum  13686  geoisumr  13687  mertenslem1  13693  mertenslem2  13694  mertens  13695  eff  13817  efcvg  13820  reefcl  13822  efcj  13827  eftlub  13844  effsumlt  13846  eflegeo  13856  eirrlem  13937  ruclem6  13968  dvdsmod  14043  bitsinv1lem  14091  sadcf  14103  sadadd3  14111  smupf  14128  alginv  14204  algcvg  14205  algcvga  14208  algfx  14209  eucalgcvga  14215  eucalg  14216  phiprmpw  14306  fermltl  14314  iserodd  14359  pcpre1  14366  qexpz  14420  prmreclem4  14437  vdwapun  14492  odf1  16584  srgbinomlem4  17194  evlslem1  18184  cpmadugsumlemF  19377  dvnff  22326  dgrcl  22630  dgrub  22631  dgrlb  22633  elqaalem2  22716  elqaalem3  22717  geolim3  22735  tayl0  22757  dvtaylp  22765  radcnvlem1  22808  radcnvlem3  22810  radcnv0  22811  radcnvlt2  22814  pserulm  22817  psercn2  22818  pserdvlem2  22823  pserdv2  22825  abelthlem4  22829  abelthlem5  22830  abelthlem6  22831  abelthlem7  22833  abelthlem8  22834  abelthlem9  22835  cosne0  22917  logtayl  23041  leibpi  23273  leibpisum  23274  log2cnv  23275  log2tlbnd  23276  basellem3  23356  dchrptlem2  23540  bcmono  23552  lgslem4  23574  lgsne0  23608  numclwwlkovf2ex  25086  archiabllem1b  27736  oddpwdc  28293  ballotlemfval0  28434  risefacval2  29132  fallfacval2  29133  binomfallfaclem2  29162  bpolydiflem  29816  itg2addnclem2  30067  rmynn  30894  jm2.24nn  30897  jm2.17c  30900  jm2.24  30901  acongrep  30918  acongeq  30921  dvdsabsmod0  30928  jm2.18  30930  jm2.23  30938  jm2.20nn  30939  jm2.27a  30947  jm2.27c  30949  rmydioph  30956  hashnzfz  31225  bccbc  31250  binomcxplemnn0  31254  binomcxplemrat  31255  binomcxplemnotnn0  31261  mccllem  31605  expfac  31663  sinaover2ne0  31668  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  stoweidlem11  31793  stoweidlem26  31808  stoweidlem34  31816  stirlinglem5  31860  fourierdlem11  31900  fourierdlem12  31901  fourierdlem14  31903  fourierdlem15  31904  fourierdlem24  31913  fourierdlem25  31914  fourierdlem36  31925  fourierdlem37  31926  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem64  31953  fourierdlem69  31958  fourierdlem73  31962  fourierdlem79  31968  fourierdlem81  31970  fourierdlem92  31981  fourierdlem93  31982  fourierdlem111  32000  elaa2lem  32016  etransclem3  32020  etransclem7  32024  etransclem10  32027  etransclem24  32041  etransclem27  32044  etransclem35  32052  etransclem44  32061  etransclem46  32063  etransclem47  32064  etransclem48  32065  2ffzoeq  32341  0even  32737  2zrngamgm  32745  altgsumbcALT  32942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator