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

Theorem 0nn0 9977
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 2286 . 2  |-  0  =  0
2 elnn0 9964 . . . 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 1625    e. wcel 1687   0cc0 8734   NNcn 9743   NN0cn0 9962
This theorem is referenced by:  nn0ind-raph  10109  numlti  10145  nummul1c  10157  decaddc2  10164  decaddi  10165  decaddci  10166  decaddci2  10167  6p5e11  10171  7p4e11  10173  8p3e11  10177  9p2e11  10183  10p10e20  10191  exple1  11157  nn0opth2  11283  faclbnd4lem3  11304  bcn1  11321  bccl  11330  hasheq0  11349  hashbc  11387  iswrdi  11413  s1cl  11437  s1fv  11442  splfv2a  11467  wrdeqs1cat  11471  s2fv0  11531  s3fv0  11534  fsumnn0cl  12205  binom  12284  bcxmas  12290  isumnn0nn  12297  climcndslem1  12304  geoser  12321  geomulcvg  12328  ef0lem  12356  ege2le3  12367  ef4p  12389  efgt1p2  12390  efgt1p  12391  ruclem11  12514  nthruz  12526  ndvdssub  12602  bits0  12615  0bits  12626  sadcf  12640  sadc0  12641  sadcaddlem  12644  sadcadd  12645  sadadd2lem  12646  sadadd2  12647  smupf  12665  smup0  12666  smumullem  12679  gcdcl  12692  nn0seqcvgd  12736  algcvg  12742  eucalg  12753  pclem  12887  pcfac  12943  vdwap0  13019  vdwap1  13020  vdwlem6  13029  hashbc0  13048  0hashbc  13050  0ram  13063  0ramcl  13066  ramz2  13067  ramz  13068  ramcl  13072  dec5dvds2  13076  2exp16  13099  11prm  13112  37prm  13118  43prm  13119  83prm  13120  139prm  13121  163prm  13122  317prm  13123  631prm  13124  1259lem1  13125  1259lem2  13126  1259lem3  13127  1259lem4  13128  1259lem5  13129  2503lem1  13131  2503lem2  13132  2503lem3  13133  2503prm  13134  4001lem1  13135  4001lem2  13136  4001lem3  13137  4001lem4  13138  4001prm  13139  odrngstr  13307  imasvalstr  13348  ipostr  14252  gsumws1  14458  oddvdsnn0  14855  pgp0  14903  sylow1lem1  14905  cyggex2  15179  psrbas  16120  psrlidm  16144  psrridm  16145  mvridlem  16160  mvrf1  16166  mplcoe3  16206  mplcoe2  16207  ltbwe  16210  psrbag0  16231  psrbagsn  16232  00ply1bas  16314  ply1plusgfvi  16316  coe1sclmul  16354  coe1sclmul2  16356  coe1scl  16358  ply1sclid  16359  cnfldstr  16375  nn0subm  16423  expmhm  16445  znf1o  16501  zzngim  16502  cygznlem1  16516  cygznlem2a  16517  cygznlem3  16519  cygth  16521  thlle  16593  dscmet  18091  itgcnlem  19140  dvn0  19269  dvn1  19271  cpncn  19281  dveflem  19322  c1lip2  19341  evlslem1  19395  tdeglem4  19442  deg1le0  19493  ply1divex  19518  ply1rem  19545  fta1g  19549  plyconst  19584  plypf1  19590  plyco  19619  0dgr  19623  0dgrb  19624  coefv0  19625  dgreq0  19642  vieta1lem2  19687  vieta1  19688  aareccl  19702  aannenlem2  19705  taylthlem1  19748  radcnv0  19788  abelthlem6  19808  abelthlem9  19812  logtayl  20003  cxp0  20013  cxpeq  20093  leibpilem2  20233  leibpi  20234  log2ublem3  20240  log2ub  20241  birthday  20245  divsqrsumlem  20270  sqff1o  20416  ppiublem2  20438  chtublem  20446  bclbnd  20515  bpos1  20518  bposlem8  20526  lgsval  20535  dchrisum0flblem1  20653  dchrisum0flb  20655  ostth2lem2  20779  1kp2ke3k  20810  subfac0  23114  subfacval2  23124  subfaclim  23125  cvmliftlem7  23228  cvmliftlem13  23233  eupa0  23304  konigsberg  23317  relexp0  23431  relexp1  23433  rtrclreclem.refl  23447  bpoly0  24194  bpoly2  24201  bpoly3  24202  bpoly4  24203  fsumcube  24204  empklst  25410  heiborlem4  25939  heiborlem10  25945  nacsfix  26188  diophrw  26239  pell1qr1  26357  monotoddzzfi  26428  jm2.23  26490  hbtlem5  26733  mncn0  26745  aaitgo  26768  psgnunilem2  26819  psgnunilem3  26820  mon1pid  26925  wallispilem2  27216  wallispi2lem2  27222  stirlinglem5  27228  stirlinglem7  27230
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-mulcl 8796  ax-i2m1 8802
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-v 2793  df-un 3160  df-sn 3649  df-n0 9963
  Copyright terms: Public domain W3C validator