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

Theorem 0nn0 10835
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
0nn0

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2457 . 2
2 elnn0 10822 . . . 4
32biimpri 206 . . 3
43olcs 395 . 2
51, 4ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  \/wo 368  =wceq 1395  e.wcel 1818  0cc0 9513   cn 10561   cn0 10820
This theorem is referenced by:  nn0ind-raph  10989  numlti  11028  nummul1c  11040  decaddc2  11047  decaddi  11048  decaddci  11049  decaddci2  11050  6p5e11  11054  7p4e11  11056  8p3e11  11060  9p2e11  11066  10p10e20  11074  0elfz  11802  4fvwrd4  11822  ssnn0fi  12094  fsuppmapnn0fiubex  12098  exple1  12225  nn0opth2  12352  faclbnd4lem3  12373  bc0k  12389  bcn1  12391  bccl  12400  hasheq0  12433  hashrabrsn  12440  hashbc  12502  brfi1uzind  12532  brfi1ind  12533  iswrdi  12552  s1fv  12619  ccat2s1fst  12643  2swrdeqwrdeq  12678  wrdeqs1cat  12700  splfv2a  12732  repsw0  12749  0csh0  12764  repswcshw  12780  cshw1  12790  s2fv0  12850  s3fv0  12853  fsumnn0cl  13558  binom  13642  bcxmas  13647  isumnn0nn  13654  climcndslem1  13661  geoser  13678  geomulcvg  13685  ef0lem  13814  ege2le3  13825  ef4p  13848  efgt1p2  13849  efgt1p  13850  ruclem11  13973  nthruz  13985  ndvdssub  14065  bits0  14078  0bits  14089  sadcf  14103  sadc0  14104  sadcaddlem  14107  sadcadd  14108  sadadd2lem  14109  sadadd2  14110  smupf  14128  smup0  14129  smumullem  14142  gcdcl  14155  nn0seqcvgd  14199  algcvg  14205  eucalg  14216  pclem  14362  pcfac  14418  vdwap0  14494  vdwap1  14495  vdwlem6  14504  hashbc0  14523  0ram  14538  0ramcl  14541  ramz2  14542  ramz  14543  ramcl  14547  dec5dvds2  14551  2exp16  14575  11prm  14600  37prm  14606  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem2  14614  1259lem3  14615  1259lem4  14616  1259lem5  14617  2503lem1  14619  2503lem2  14620  2503lem3  14621  2503prm  14622  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001lem4  14626  4001prm  14627  odrngstr  14804  imasvalstr  14849  ipostr  15783  gsumws1  16007  psgnunilem2  16520  psgnunilem3  16521  oddvdsnn0  16568  pgp0  16616  sylow1lem1  16618  cyggex2  16899  telgsums  17022  srgbinomlem3  17193  srgbinomlem4  17194  srgbinom  17196  snifpsrbag  18015  fczpsrbag  18016  psrbasOLD  18031  psrlidm  18056  psrlidmOLD  18057  psrridmOLD  18059  mvridlemOLD  18075  mvrf1  18081  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  ltbwe  18137  psrbag0  18159  psrbagsn  18160  evlslem1  18184  00ply1bas  18281  ply1plusgfvi  18283  coe1sclmul  18323  coe1sclmul2  18325  coe1scl  18328  ply1sclid  18329  ply1idvr1  18334  cply1coe0bi  18342  cnfldstr  18422  nn0subm  18473  expmhm  18485  nn0srg  18486  znf1o  18590  zzngim  18591  cygznlem1  18605  cygznlem2a  18606  cygznlem3  18608  cygth  18610  thlle  18728  cpm2mf  19253  m2cpminvid2lem  19255  m2cpminvid2  19256  m2cpmfo  19257  decpmatid  19271  pmatcollpw3  19285  pmatcollpw3fi1lem1  19287  pmatcollpwscmatlem1  19290  pmatcollpwscmatlem2  19291  idpm2idmp  19302  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  cpmadugsumlemF  19377  dscmet  21093  itgcnlem  22196  dvn0  22327  dvn1  22329  cpncn  22339  dveflem  22380  c1lip2  22399  tdeglem4  22458  deg1le0  22512  ply1divex  22537  ply1rem  22564  fta1g  22568  plyconst  22603  plypf1  22609  plyco  22638  0dgr  22642  0dgrb  22643  coefv0  22645  dgreq0  22662  vieta1lem2  22707  vieta1  22708  aareccl  22722  aannenlem2  22725  taylthlem1  22768  radcnv0  22811  abelthlem6  22831  abelthlem9  22835  logtayl  23041  cxp0  23051  cxpeq  23131  leibpilem2  23272  leibpi  23273  log2ublem3  23279  log2ub  23280  birthday  23284  divsqrtsumlem  23309  sqff1o  23456  ppiublem2  23478  chtublem  23486  bclbnd  23555  bpos1  23558  bposlem8  23566  lgsval  23575  dchrisum0flblem1  23693  dchrisum0flb  23695  ostth2lem2  23819  usgraex0elv  24396  usgrafisbase  24414  wlkonwlk  24537  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv  24667  wwlkn0  24689  wwlkn0s  24705  clwwlkn0  24774  clwwlkf1  24796  erclwwlkref  24813  0egra0rgra  24936  rusgranumwlkb0  24953  rusgra0edg  24955  eupa0  24974  konigsberg  24987  1kp2ke3k  25167  nn0min  27611  fsumcvg4  27932  log2le1  28023  oddpwdc  28293  eulerpartlems  28299  eulerpartlemb  28307  eulerpartlemt  28310  eulerpartgbij  28311  eulerpartlemmf  28314  eulerpartlemgf  28318  eulerpartlemgs2  28319  eulerpartlemn  28320  fib0  28338  fib1  28339  fibp1  28340  ofs1  28499  ofcs1  28500  signsply0  28508  signsvvf  28536  dmgmn0  28568  lgambdd  28579  subfac0  28621  subfacval2  28631  subfaclim  28632  cvmliftlem7  28736  cvmliftlem13  28741  relexp0  29052  relexp1  29054  rtrclreclem.refl  29067  risefac0  29149  fallfac0  29150  risefac1  29155  fallfac1  29156  binomfallfaclem2  29162  binomfallfac  29163  bpoly0  29812  bpoly2  29819  bpoly3  29820  bpoly4  29821  fsumcube  29822  heiborlem4  30310  heiborlem10  30316  nacsfix  30644  diophrw  30692  pell1qr1  30807  monotoddzzfi  30878  jm2.23  30938  hbtlem5  31077  mncn0  31088  aaitgo  31111  mon1pid  31165  lcmcl  31207  bccn0  31248  bccn1  31249  binomcxplemradcnv  31257  binomcxplemnotnn0  31261  dvnmul  31740  dvnprodlem3  31745  wallispilem2  31848  wallispi2lem2  31854  stirlinglem5  31860  stirlinglem7  31862  fourierdlem83  31972  fourierdlem112  32001  fouriersw  32014  elaa2lem  32016  elaa2  32017  etransclem48  32065  etransc  32066  usgra2pthlem1  32353  uhgrepe  32378  usgo0fis  32438  usgo0fisALT  32439  ssnn0ssfz  32938
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-mulcl 9575  ax-i2m1 9581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  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-v 3111  df-un 3480  df-sn 4030  df-n0 10821
  Copyright terms: Public domain W3C validator