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

Theorem 0nn0 10236
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 2436 . 2  |-  0  =  0
2 elnn0 10223 . . . 4  |-  ( 0  e.  NN0  <->  ( 0  e.  NN  \/  0  =  0 ) )
32biimpri 198 . . 3  |-  ( ( 0  e.  NN  \/  0  =  0 )  ->  0  e.  NN0 )
43olcs 385 . 2  |-  ( 0  =  0  ->  0  e.  NN0 )
51, 4ax-mp 8 1  |-  0  e.  NN0
Colors of variables: wff set class
Syntax hints:    \/ wo 358    = wceq 1652    e. wcel 1725   0cc0 8990   NNcn 10000   NN0cn0 10221
This theorem is referenced by:  nn0ind-raph  10370  numlti  10406  nummul1c  10418  decaddc2  10425  decaddi  10426  decaddci  10427  decaddci2  10428  6p5e11  10432  7p4e11  10434  8p3e11  10438  9p2e11  10444  10p10e20  10452  4fvwrd4  11121  injresinjlem  11199  exple1  11439  nn0opth2  11565  faclbnd4lem3  11586  bc0k  11602  bcn1  11604  bccl  11613  hasheq0  11644  hashrabrsn  11648  hashbc  11702  brfi1uzind  11715  brfi1ind  11716  iswrdi  11731  s1cl  11755  s1fv  11760  splfv2a  11785  wrdeqs1cat  11789  s2fv0  11849  s3fv0  11852  fsumnn0cl  12530  binom  12609  bcxmas  12615  isumnn0nn  12622  climcndslem1  12629  geoser  12646  geomulcvg  12653  ef0lem  12681  ege2le3  12692  ef4p  12714  efgt1p2  12715  efgt1p  12716  ruclem11  12839  nthruz  12851  ndvdssub  12927  bits0  12940  0bits  12951  sadcf  12965  sadc0  12966  sadcaddlem  12969  sadcadd  12970  sadadd2lem  12971  sadadd2  12972  smupf  12990  smup0  12991  smumullem  13004  gcdcl  13017  nn0seqcvgd  13061  algcvg  13067  eucalg  13078  pclem  13212  pcfac  13268  vdwap0  13344  vdwap1  13345  vdwlem6  13354  hashbc0  13373  0ram  13388  0ramcl  13391  ramz2  13392  ramz  13393  ramcl  13397  dec5dvds2  13401  2exp16  13424  11prm  13437  37prm  13443  43prm  13444  83prm  13445  139prm  13446  163prm  13447  317prm  13448  631prm  13449  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  1259lem5  13454  2503lem1  13456  2503lem2  13457  2503lem3  13458  2503prm  13459  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  4001prm  13464  odrngstr  13634  imasvalstr  13675  ipostr  14579  gsumws1  14785  oddvdsnn0  15182  pgp0  15230  sylow1lem1  15232  cyggex2  15506  psrbas  16443  psrlidm  16467  psrridm  16468  mvridlem  16483  mvrf1  16489  mplcoe3  16529  mplcoe2  16530  ltbwe  16533  psrbag0  16554  psrbagsn  16555  00ply1bas  16634  ply1plusgfvi  16636  coe1sclmul  16674  coe1sclmul2  16676  coe1scl  16678  ply1sclid  16679  cnfldstr  16705  nn0subm  16754  expmhm  16776  znf1o  16832  zzngim  16833  cygznlem1  16847  cygznlem2a  16848  cygznlem3  16850  cygth  16852  thlle  16924  dscmet  18620  itgcnlem  19681  dvn0  19810  dvn1  19812  cpncn  19822  dveflem  19863  c1lip2  19882  evlslem1  19936  tdeglem4  19983  deg1le0  20034  ply1divex  20059  ply1rem  20086  fta1g  20090  plyconst  20125  plypf1  20131  plyco  20160  0dgr  20164  0dgrb  20165  coefv0  20166  dgreq0  20183  vieta1lem2  20228  vieta1  20229  aareccl  20243  aannenlem2  20246  taylthlem1  20289  radcnv0  20332  abelthlem6  20352  abelthlem9  20356  logtayl  20551  cxp0  20561  cxpeq  20641  leibpilem2  20781  leibpi  20782  log2ublem3  20788  log2ub  20789  birthday  20793  divsqrsumlem  20818  sqff1o  20965  ppiublem2  20987  chtublem  20995  bclbnd  21064  bpos1  21067  bposlem8  21075  lgsval  21084  dchrisum0flblem1  21202  dchrisum0flb  21204  ostth2lem2  21328  usgraex0elv  21415  usgrafisbase  21428  wlkonwlk  21535  cyclnspth  21618  cyclispthon  21620  3v3e3cycl1  21631  4cycl4v4e  21653  4cycl4dv  21654  eupa0  21696  konigsberg  21709  1kp2ke3k  21754  log2le1  24407  dmgmn0  24810  lgambdd  24821  subfac0  24863  subfacval2  24873  subfaclim  24874  cvmliftlem7  24978  cvmliftlem13  24983  relexp0  25129  relexp1  25131  rtrclreclem.refl  25144  risefac0  25343  fallfac0  25344  risefac1  25349  fallfac1  25350  binomfallfaclem2  25356  binomfallfac  25357  bpoly0  26096  bpoly2  26103  bpoly3  26104  bpoly4  26105  fsumcube  26106  heiborlem4  26523  heiborlem10  26529  nacsfix  26766  diophrw  26817  pell1qr1  26934  monotoddzzfi  27005  jm2.23  27067  hbtlem5  27309  mncn0  27321  aaitgo  27344  psgnunilem2  27395  psgnunilem3  27396  mon1pid  27501  wallispilem2  27791  wallispi2lem2  27797  stirlinglem5  27803  stirlinglem7  27805  0elfz  28111  cshw0  28238  2cshw2lem2  28253  swrdtrcfvl  28265  cshw1  28275  usgra2pthlem1  28310  0egra0rgra  28375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-mulcl 9052  ax-i2m1 9058
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-un 3325  df-sn 3820  df-n0 10222
  Copyright terms: Public domain W3C validator