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

Theorem 0nn0 10192
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 2404 . 2  |-  0  =  0
2 elnn0 10179 . . . 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 1649    e. wcel 1721   0cc0 8946   NNcn 9956   NN0cn0 10177
This theorem is referenced by:  nn0ind-raph  10326  numlti  10362  nummul1c  10374  decaddc2  10381  decaddi  10382  decaddci  10383  decaddci2  10384  6p5e11  10388  7p4e11  10390  8p3e11  10394  9p2e11  10400  10p10e20  10408  4fvwrd4  11076  injresinjlem  11154  exple1  11394  nn0opth2  11520  faclbnd4lem3  11541  bc0k  11557  bcn1  11559  bccl  11568  hasheq0  11599  hashrabrsn  11603  hashbc  11657  brfi1uzind  11670  brfi1ind  11671  iswrdi  11686  s1cl  11710  s1fv  11715  splfv2a  11740  wrdeqs1cat  11744  s2fv0  11804  s3fv0  11807  fsumnn0cl  12485  binom  12564  bcxmas  12570  isumnn0nn  12577  climcndslem1  12584  geoser  12601  geomulcvg  12608  ef0lem  12636  ege2le3  12647  ef4p  12669  efgt1p2  12670  efgt1p  12671  ruclem11  12794  nthruz  12806  ndvdssub  12882  bits0  12895  0bits  12906  sadcf  12920  sadc0  12921  sadcaddlem  12924  sadcadd  12925  sadadd2lem  12926  sadadd2  12927  smupf  12945  smup0  12946  smumullem  12959  gcdcl  12972  nn0seqcvgd  13016  algcvg  13022  eucalg  13033  pclem  13167  pcfac  13223  vdwap0  13299  vdwap1  13300  vdwlem6  13309  hashbc0  13328  0ram  13343  0ramcl  13346  ramz2  13347  ramz  13348  ramcl  13352  dec5dvds2  13356  2exp16  13379  11prm  13392  37prm  13398  43prm  13399  83prm  13400  139prm  13401  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  odrngstr  13589  imasvalstr  13630  ipostr  14534  gsumws1  14740  oddvdsnn0  15137  pgp0  15185  sylow1lem1  15187  cyggex2  15461  psrbas  16398  psrlidm  16422  psrridm  16423  mvridlem  16438  mvrf1  16444  mplcoe3  16484  mplcoe2  16485  ltbwe  16488  psrbag0  16509  psrbagsn  16510  00ply1bas  16589  ply1plusgfvi  16591  coe1sclmul  16629  coe1sclmul2  16631  coe1scl  16633  ply1sclid  16634  cnfldstr  16660  nn0subm  16709  expmhm  16731  znf1o  16787  zzngim  16788  cygznlem1  16802  cygznlem2a  16803  cygznlem3  16805  cygth  16807  thlle  16879  dscmet  18573  itgcnlem  19634  dvn0  19763  dvn1  19765  cpncn  19775  dveflem  19816  c1lip2  19835  evlslem1  19889  tdeglem4  19936  deg1le0  19987  ply1divex  20012  ply1rem  20039  fta1g  20043  plyconst  20078  plypf1  20084  plyco  20113  0dgr  20117  0dgrb  20118  coefv0  20119  dgreq0  20136  vieta1lem2  20181  vieta1  20182  aareccl  20196  aannenlem2  20199  taylthlem1  20242  radcnv0  20285  abelthlem6  20305  abelthlem9  20309  logtayl  20504  cxp0  20514  cxpeq  20594  leibpilem2  20734  leibpi  20735  log2ublem3  20741  log2ub  20742  birthday  20746  divsqrsumlem  20771  sqff1o  20918  ppiublem2  20940  chtublem  20948  bclbnd  21017  bpos1  21020  bposlem8  21028  lgsval  21037  dchrisum0flblem1  21155  dchrisum0flb  21157  ostth2lem2  21281  usgraex0elv  21368  usgrafisbase  21381  wlkonwlk  21488  cyclnspth  21571  cyclispthon  21573  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv  21607  eupa0  21649  konigsberg  21662  1kp2ke3k  21707  log2le1  24360  dmgmn0  24763  lgambdd  24774  subfac0  24816  subfacval2  24826  subfaclim  24827  cvmliftlem7  24931  cvmliftlem13  24936  relexp0  25082  relexp1  25084  rtrclreclem.refl  25097  risefac0  25295  fallfac0  25296  risefac1  25299  fallfac1  25300  binomfallfaclem2  25307  binomfallfac  25308  bpoly0  26000  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  heiborlem4  26413  heiborlem10  26419  nacsfix  26656  diophrw  26707  pell1qr1  26824  monotoddzzfi  26895  jm2.23  26957  hbtlem5  27200  mncn0  27212  aaitgo  27235  psgnunilem2  27286  psgnunilem3  27287  mon1pid  27392  wallispilem2  27682  wallispi2lem2  27688  stirlinglem5  27694  stirlinglem7  27696  0elfz  27983  swrdccatin12lem3  28024  usgra2pthlem1  28040
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-i2m1 9014
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-sn 3780  df-n0 10178
  Copyright terms: Public domain W3C validator