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

Theorem 0nn0 9912
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 9899 . . . 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 8670   NNcn 9679   NN0cn0 9897
This theorem is referenced by:  nn0ind-raph  10044  numlti  10080  nummul1c  10092  decaddc2  10099  decaddi  10100  decaddci  10101  decaddci2  10102  6p5e11  10106  7p4e11  10108  8p3e11  10112  9p2e11  10118  10p10e20  10126  exple1  11092  nn0opth2  11218  faclbnd4lem3  11239  bcn1  11256  bccl  11265  hasheq0  11284  hashbc  11321  iswrdi  11347  s1cl  11371  s1fv  11376  splfv2a  11401  wrdeqs1cat  11405  s2fv0  11465  s3fv0  11468  fsumnn0cl  12139  binom  12218  bcxmas  12224  isumnn0nn  12228  climcndslem1  12235  geoser  12252  geomulcvg  12259  ef0lem  12287  ege2le3  12298  ef4p  12320  efgt1p2  12321  efgt1p  12322  ruclem11  12445  nthruz  12457  ndvdssub  12533  bits0  12546  0bits  12557  sadcf  12571  sadc0  12572  sadcaddlem  12575  sadcadd  12576  sadadd2lem  12577  sadadd2  12578  smupf  12596  smup0  12597  smumullem  12610  gcdcl  12623  nn0seqcvgd  12667  algcvg  12673  eucalg  12684  pclem  12818  pcfac  12874  vdwap0  12950  vdwap1  12951  vdwlem6  12960  hashbc0  12979  0hashbc  12981  0ram  12994  0ramcl  12997  ramz2  12998  ramz  12999  ramcl  13003  dec5dvds2  13007  2exp16  13030  11prm  13043  37prm  13049  43prm  13050  83prm  13051  139prm  13052  163prm  13053  317prm  13054  631prm  13055  1259lem1  13056  1259lem2  13057  1259lem3  13058  1259lem4  13059  1259lem5  13060  2503lem1  13062  2503lem2  13063  2503lem3  13064  2503prm  13065  4001lem1  13066  4001lem2  13067  4001lem3  13068  4001lem4  13069  4001prm  13070  odrngstr  13238  imasvalstr  13279  ipostr  14183  gsumws1  14389  oddvdsnn0  14786  pgp0  14834  sylow1lem1  14836  cyggex2  15110  psrbas  16051  psrlidm  16075  psrridm  16076  mvridlem  16091  mvrf1  16097  mplcoe3  16137  mplcoe2  16138  ltbwe  16141  psrbag0  16162  psrbagsn  16163  00ply1bas  16245  ply1plusgfvi  16247  coe1sclmul  16285  coe1sclmul2  16287  coe1scl  16289  ply1sclid  16290  cnfldstr  16306  nn0subm  16354  expmhm  16376  znf1o  16432  zzngim  16433  cygznlem1  16447  cygznlem2a  16448  cygznlem3  16450  cygth  16452  thlle  16524  dscmet  18022  itgcnlem  19071  dvn0  19200  dvn1  19202  cpncn  19212  dveflem  19253  c1lip2  19272  evlslem1  19326  tdeglem4  19373  deg1le0  19424  ply1divex  19449  ply1rem  19476  fta1g  19480  plyconst  19515  plypf1  19521  plyco  19550  0dgr  19554  0dgrb  19555  coefv0  19556  dgreq0  19573  vieta1lem2  19618  vieta1  19619  aareccl  19633  aannenlem2  19636  taylthlem1  19679  radcnv0  19719  abelthlem6  19739  abelthlem9  19743  logtayl  19934  cxp0  19944  cxpeq  20024  leibpilem2  20164  leibpi  20165  log2ublem3  20171  log2ub  20172  birthday  20176  divsqrsumlem  20201  sqff1o  20347  ppiublem2  20369  chtublem  20377  bclbnd  20446  bpos1  20449  bposlem8  20457  lgsval  20466  dchrisum0flblem1  20584  dchrisum0flb  20586  ostth2lem2  20710  1kp2ke3k  20741  subfac0  23045  subfacval2  23055  subfaclim  23056  cvmliftlem7  23159  cvmliftlem13  23164  eupa0  23235  konigsberg  23248  relexp0  23362  relexp1  23364  rtrclreclem.refl  23378  bpoly0  24125  bpoly2  24132  bpoly3  24133  bpoly4  24134  fsumcube  24135  empklst  25341  heiborlem4  25870  heiborlem10  25876  nacsfix  26119  diophrw  26170  pell1qr1  26288  monotoddzzfi  26359  jm2.23  26421  hbtlem5  26664  mncn0  26676  aaitgo  26699  psgnunilem2  26750  psgnunilem3  26751  mon1pid  26856
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 8728  ax-icn 8729  ax-addcl 8730  ax-mulcl 8732  ax-i2m1 8738
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 2742  df-un 3099  df-sn 3587  df-n0 9898
  Copyright terms: Public domain W3C validator