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

Theorem 0nn0 9996
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 2296 . 2  |-  0  =  0
2 elnn0 9983 . . . 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 1632    e. wcel 1696   0cc0 8753   NNcn 9762   NN0cn0 9981
This theorem is referenced by:  nn0ind-raph  10128  numlti  10164  nummul1c  10176  decaddc2  10183  decaddi  10184  decaddci  10185  decaddci2  10186  6p5e11  10190  7p4e11  10192  8p3e11  10196  9p2e11  10202  10p10e20  10210  exple1  11177  nn0opth2  11303  faclbnd4lem3  11324  bcn1  11341  bccl  11350  hasheq0  11369  hashbc  11407  iswrdi  11433  s1cl  11457  s1fv  11462  splfv2a  11487  wrdeqs1cat  11491  s2fv0  11551  s3fv0  11554  fsumnn0cl  12225  binom  12304  bcxmas  12310  isumnn0nn  12317  climcndslem1  12324  geoser  12341  geomulcvg  12348  ef0lem  12376  ege2le3  12387  ef4p  12409  efgt1p2  12410  efgt1p  12411  ruclem11  12534  nthruz  12546  ndvdssub  12622  bits0  12635  0bits  12646  sadcf  12660  sadc0  12661  sadcaddlem  12664  sadcadd  12665  sadadd2lem  12666  sadadd2  12667  smupf  12685  smup0  12686  smumullem  12699  gcdcl  12712  nn0seqcvgd  12756  algcvg  12762  eucalg  12773  pclem  12907  pcfac  12963  vdwap0  13039  vdwap1  13040  vdwlem6  13049  hashbc0  13068  0hashbc  13070  0ram  13083  0ramcl  13086  ramz2  13087  ramz  13088  ramcl  13092  dec5dvds2  13096  2exp16  13119  11prm  13132  37prm  13138  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  odrngstr  13327  imasvalstr  13368  ipostr  14272  gsumws1  14478  oddvdsnn0  14875  pgp0  14923  sylow1lem1  14925  cyggex2  15199  psrbas  16140  psrlidm  16164  psrridm  16165  mvridlem  16180  mvrf1  16186  mplcoe3  16226  mplcoe2  16227  ltbwe  16230  psrbag0  16251  psrbagsn  16252  00ply1bas  16334  ply1plusgfvi  16336  coe1sclmul  16374  coe1sclmul2  16376  coe1scl  16378  ply1sclid  16379  cnfldstr  16395  nn0subm  16443  expmhm  16465  znf1o  16521  zzngim  16522  cygznlem1  16536  cygznlem2a  16537  cygznlem3  16539  cygth  16541  thlle  16613  dscmet  18111  itgcnlem  19160  dvn0  19289  dvn1  19291  cpncn  19301  dveflem  19342  c1lip2  19361  evlslem1  19415  tdeglem4  19462  deg1le0  19513  ply1divex  19538  ply1rem  19565  fta1g  19569  plyconst  19604  plypf1  19610  plyco  19639  0dgr  19643  0dgrb  19644  coefv0  19645  dgreq0  19662  vieta1lem2  19707  vieta1  19708  aareccl  19722  aannenlem2  19725  taylthlem1  19768  radcnv0  19808  abelthlem6  19828  abelthlem9  19832  logtayl  20023  cxp0  20033  cxpeq  20113  leibpilem2  20253  leibpi  20254  log2ublem3  20260  log2ub  20261  birthday  20265  divsqrsumlem  20290  sqff1o  20436  ppiublem2  20458  chtublem  20466  bclbnd  20535  bpos1  20538  bposlem8  20546  lgsval  20555  dchrisum0flblem1  20673  dchrisum0flb  20675  ostth2lem2  20799  1kp2ke3k  20849  log2le1  23424  subfac0  23723  subfacval2  23733  subfaclim  23734  cvmliftlem7  23837  cvmliftlem13  23842  eupa0  23913  konigsberg  23926  relexp0  24040  relexp1  24042  rtrclreclem.refl  24056  bpoly0  24857  bpoly2  24864  bpoly3  24865  bpoly4  24866  fsumcube  24867  empklst  26112  heiborlem4  26641  heiborlem10  26647  nacsfix  26890  diophrw  26941  pell1qr1  27059  monotoddzzfi  27130  jm2.23  27192  hbtlem5  27435  mncn0  27447  aaitgo  27470  psgnunilem2  27521  psgnunilem3  27522  mon1pid  27627  wallispilem2  27918  wallispi2lem2  27924  stirlinglem5  27930  stirlinglem7  27932  injresinjlem  28214  4fvwrd4  28220  usgraex0elv  28262  wlkonwlk  28334  cyclnspth  28376  cyclispthon  28378  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv  28413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-mulcl 8815  ax-i2m1 8821
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-n0 9982
  Copyright terms: Public domain W3C validator