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

Theorem 0nn0 9933
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 2256 . 2  |-  0  =  0
2 elnn0 9920 . . . 4  |-  ( 0  e.  NN0  <->  ( 0  e.  NN  \/  0  =  0 ) )
32biimpri 199 . . 3  |-  ( ( 0  e.  NN  \/  0  =  0 )  ->  0  e.  NN0 )
43olcs 386 . 2  |-  ( 0  =  0  ->  0  e.  NN0 )
51, 4ax-mp 10 1  |-  0  e.  NN0
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621   0cc0 8691   NNcn 9700   NN0cn0 9918
This theorem is referenced by:  nn0ind-raph  10065  numlti  10101  nummul1c  10113  decaddc2  10120  decaddi  10121  decaddci  10122  decaddci2  10123  6p5e11  10127  7p4e11  10129  8p3e11  10133  9p2e11  10139  10p10e20  10147  exple1  11113  nn0opth2  11239  faclbnd4lem3  11260  bcn1  11277  bccl  11286  hasheq0  11305  hashbc  11342  iswrdi  11368  s1cl  11392  s1fv  11397  splfv2a  11422  wrdeqs1cat  11426  s2fv0  11486  s3fv0  11489  fsumnn0cl  12160  binom  12239  bcxmas  12245  isumnn0nn  12249  climcndslem1  12256  geoser  12273  geomulcvg  12280  ef0lem  12308  ege2le3  12319  ef4p  12341  efgt1p2  12342  efgt1p  12343  ruclem11  12466  nthruz  12478  ndvdssub  12554  bits0  12567  0bits  12578  sadcf  12592  sadc0  12593  sadcaddlem  12596  sadcadd  12597  sadadd2lem  12598  sadadd2  12599  smupf  12617  smup0  12618  smumullem  12631  gcdcl  12644  nn0seqcvgd  12688  algcvg  12694  eucalg  12705  pclem  12839  pcfac  12895  vdwap0  12971  vdwap1  12972  vdwlem6  12981  hashbc0  13000  0hashbc  13002  0ram  13015  0ramcl  13018  ramz2  13019  ramz  13020  ramcl  13024  dec5dvds2  13028  2exp16  13051  11prm  13064  37prm  13070  43prm  13071  83prm  13072  139prm  13073  163prm  13074  317prm  13075  631prm  13076  1259lem1  13077  1259lem2  13078  1259lem3  13079  1259lem4  13080  1259lem5  13081  2503lem1  13083  2503lem2  13084  2503lem3  13085  2503prm  13086  4001lem1  13087  4001lem2  13088  4001lem3  13089  4001lem4  13090  4001prm  13091  odrngstr  13259  imasvalstr  13300  ipostr  14204  gsumws1  14410  oddvdsnn0  14807  pgp0  14855  sylow1lem1  14857  cyggex2  15131  psrbas  16072  psrlidm  16096  psrridm  16097  mvridlem  16112  mvrf1  16118  mplcoe3  16158  mplcoe2  16159  ltbwe  16162  psrbag0  16183  psrbagsn  16184  00ply1bas  16266  ply1plusgfvi  16268  coe1sclmul  16306  coe1sclmul2  16308  coe1scl  16310  ply1sclid  16311  cnfldstr  16327  nn0subm  16375  expmhm  16397  znf1o  16453  zzngim  16454  cygznlem1  16468  cygznlem2a  16469  cygznlem3  16471  cygth  16473  thlle  16545  dscmet  18043  itgcnlem  19092  dvn0  19221  dvn1  19223  cpncn  19233  dveflem  19274  c1lip2  19293  evlslem1  19347  tdeglem4  19394  deg1le0  19445  ply1divex  19470  ply1rem  19497  fta1g  19501  plyconst  19536  plypf1  19542  plyco  19571  0dgr  19575  0dgrb  19576  coefv0  19577  dgreq0  19594  vieta1lem2  19639  vieta1  19640  aareccl  19654  aannenlem2  19657  taylthlem1  19700  radcnv0  19740  abelthlem6  19760  abelthlem9  19764  logtayl  19955  cxp0  19965  cxpeq  20045  leibpilem2  20185  leibpi  20186  log2ublem3  20192  log2ub  20193  birthday  20197  divsqrsumlem  20222  sqff1o  20368  ppiublem2  20390  chtublem  20398  bclbnd  20467  bpos1  20470  bposlem8  20478  lgsval  20487  dchrisum0flblem1  20605  dchrisum0flb  20607  ostth2lem2  20731  1kp2ke3k  20762  subfac0  23066  subfacval2  23076  subfaclim  23077  cvmliftlem7  23180  cvmliftlem13  23185  eupa0  23256  konigsberg  23269  relexp0  23383  relexp1  23385  rtrclreclem.refl  23399  bpoly0  24146  bpoly2  24153  bpoly3  24154  bpoly4  24155  fsumcube  24156  empklst  25362  heiborlem4  25891  heiborlem10  25897  nacsfix  26140  diophrw  26191  pell1qr1  26309  monotoddzzfi  26380  jm2.23  26442  hbtlem5  26685  mncn0  26697  aaitgo  26720  psgnunilem2  26771  psgnunilem3  26772  mon1pid  26877
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-mulcl 8753  ax-i2m1 8759
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118  df-sn 3606  df-n0 9919
  Copyright terms: Public domain W3C validator