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

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

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2283 . 2  |-  0  =  0
2 elnn0 9967 . . . 4  |-  ( 0  e.  NN0  <->  ( 0  e.  NN  \/  0  =  0 ) )
32biimpri 197 . . 3  |-  ( ( 0  e.  NN  \/  0  =  0 )  ->  0  e.  NN0 )
43olcs 384 . 2  |-  ( 0  =  0  ->  0  e.  NN0 )
51, 4ax-mp 8 1  |-  0  e.  NN0
Colors of variables: wff set class
Syntax hints:    \/ wo 357    = wceq 1623    e. wcel 1684   0cc0 8737   NNcn 9746   NN0cn0 9965
This theorem is referenced by:  nn0ind-raph  10112  numlti  10148  nummul1c  10160  decaddc2  10167  decaddi  10168  decaddci  10169  decaddci2  10170  6p5e11  10174  7p4e11  10176  8p3e11  10180  9p2e11  10186  10p10e20  10194  exple1  11161  nn0opth2  11287  faclbnd4lem3  11308  bcn1  11325  bccl  11334  hasheq0  11353  hashbc  11391  iswrdi  11417  s1cl  11441  s1fv  11446  splfv2a  11471  wrdeqs1cat  11475  s2fv0  11535  s3fv0  11538  fsumnn0cl  12209  binom  12288  bcxmas  12294  isumnn0nn  12301  climcndslem1  12308  geoser  12325  geomulcvg  12332  ef0lem  12360  ege2le3  12371  ef4p  12393  efgt1p2  12394  efgt1p  12395  ruclem11  12518  nthruz  12530  ndvdssub  12606  bits0  12619  0bits  12630  sadcf  12644  sadc0  12645  sadcaddlem  12648  sadcadd  12649  sadadd2lem  12650  sadadd2  12651  smupf  12669  smup0  12670  smumullem  12683  gcdcl  12696  nn0seqcvgd  12740  algcvg  12746  eucalg  12757  pclem  12891  pcfac  12947  vdwap0  13023  vdwap1  13024  vdwlem6  13033  hashbc0  13052  0hashbc  13054  0ram  13067  0ramcl  13070  ramz2  13071  ramz  13072  ramcl  13076  dec5dvds2  13080  2exp16  13103  11prm  13116  37prm  13122  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  odrngstr  13311  imasvalstr  13352  ipostr  14256  gsumws1  14462  oddvdsnn0  14859  pgp0  14907  sylow1lem1  14909  cyggex2  15183  psrbas  16124  psrlidm  16148  psrridm  16149  mvridlem  16164  mvrf1  16170  mplcoe3  16210  mplcoe2  16211  ltbwe  16214  psrbag0  16235  psrbagsn  16236  00ply1bas  16318  ply1plusgfvi  16320  coe1sclmul  16358  coe1sclmul2  16360  coe1scl  16362  ply1sclid  16363  cnfldstr  16379  nn0subm  16427  expmhm  16449  znf1o  16505  zzngim  16506  cygznlem1  16520  cygznlem2a  16521  cygznlem3  16523  cygth  16525  thlle  16597  dscmet  18095  itgcnlem  19144  dvn0  19273  dvn1  19275  cpncn  19285  dveflem  19326  c1lip2  19345  evlslem1  19399  tdeglem4  19446  deg1le0  19497  ply1divex  19522  ply1rem  19549  fta1g  19553  plyconst  19588  plypf1  19594  plyco  19623  0dgr  19627  0dgrb  19628  coefv0  19629  dgreq0  19646  vieta1lem2  19691  vieta1  19692  aareccl  19706  aannenlem2  19709  taylthlem1  19752  radcnv0  19792  abelthlem6  19812  abelthlem9  19816  logtayl  20007  cxp0  20017  cxpeq  20097  leibpilem2  20237  leibpi  20238  log2ublem3  20244  log2ub  20245  birthday  20249  divsqrsumlem  20274  sqff1o  20420  ppiublem2  20442  chtublem  20450  bclbnd  20519  bpos1  20522  bposlem8  20530  lgsval  20539  dchrisum0flblem1  20657  dchrisum0flb  20659  ostth2lem2  20783  1kp2ke3k  20833  log2le1  23409  subfac0  23708  subfacval2  23718  subfaclim  23719  cvmliftlem7  23822  cvmliftlem13  23827  eupa0  23898  konigsberg  23911  relexp0  24025  relexp1  24027  rtrclreclem.refl  24041  bpoly0  24785  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  empklst  26009  heiborlem4  26538  heiborlem10  26544  nacsfix  26787  diophrw  26838  pell1qr1  26956  monotoddzzfi  27027  jm2.23  27089  hbtlem5  27332  mncn0  27344  aaitgo  27367  psgnunilem2  27418  psgnunilem3  27419  mon1pid  27524  wallispilem2  27815  wallispi2lem2  27821  stirlinglem5  27827  stirlinglem7  27829  usgraex0elv  28128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-i2m1 8805
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-n0 9966
  Copyright terms: Public domain W3C validator