Theorem 0nn0 10873

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
0nn0	|- 0 e. NN0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2420	. 2 |- 0 = 0
2		elnn0 10860	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 209	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 396	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 369   = wceq 1437   e. wcel 1867   0cc0 9528   NNcn 10598   NN0cn0 10858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-mulcl 9590  ax-i2m1 9596

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-un 3438  df-sn 3994  df-n0 10859

This theorem is referenced by:  nn0ind-raph  11024  numlti  11064  nummul1c  11076  decaddc2  11083  decaddi  11084  decaddci  11085  decaddci2  11086  6p5e11  11090  7p4e11  11092  8p3e11  11096  9p2e11  11102  10p10e20  11110  0elfz  11876  4fvwrd4  11896  ssnn0fi  12183  fsuppmapnn0fiubex  12190  exple1  12318  nn0opth2  12444  faclbnd4lem3  12466  bc0k  12482  bcn1  12484  bccl  12493  hasheq0  12530  hashrabrsn  12537  hashbc  12600  brfi1uzind  12630  brfi1ind  12631  iswrdi  12651  s1fv  12722  ccat2s1fst  12746  2swrdeqwrdeq  12783  wrdeqs1cat  12805  splfv2a  12837  repsw0  12854  0csh0  12869  repswcshw  12885  cshw1  12895  s2fv0  12955  s3fv0  12958  relexp0g  13053  relexpaddg  13084  rtrclreclem1  13089  fsumnn0cl  13769  binom  13855  bcxmas  13860  isumnn0nn  13867  climcndslem1  13874  geoser  13892  geomulcvg  13899  risefac0  14047  fallfac0  14048  risefac1  14053  fallfac1  14054  binomfallfaclem2  14060  binomfallfac  14061  bpoly0  14070  bpoly2  14077  bpoly3  14078  bpoly4  14079  fsumcube  14080  ef0lem  14100  ege2le3  14111  ef4p  14134  efgt1p2  14135  efgt1p  14136  ruclem11  14259  nthruz  14271  ndvdssub  14352  bits0  14365  0bits  14376  sadcf  14390  sadc0  14391  sadcaddlem  14394  sadcadd  14395  sadadd2lem  14396  sadadd2  14397  smupf  14415  smup0  14416  smumullem  14429  gcdcl  14443  nn0seqcvgd  14489  algcvg  14495  eucalg  14506  lcmcl  14526  lcmfval  14551  lcmfvalOLD  14555  lcmfcl  14561  pclem  14748  pcfac  14804  vdwap0  14886  vdwap1  14887  vdwlem6  14896  hashbc0  14917  0ram  14938  0ramcl  14941  ramz2  14942  ramz  14943  ramcl  14947  prmo0  14954  dec5dvds2  14997  2exp16  15021  11prm  15046  37prm  15052  43prm  15053  83prm  15054  139prm  15055  163prm  15056  317prm  15057  631prm  15058  1259lem1  15062  1259lem2  15063  1259lem3  15064  1259lem4  15065  1259lem5  15066  2503lem1  15068  2503lem2  15069  2503lem3  15070  2503prm  15071  4001lem1  15072  4001lem2  15073  4001lem3  15074  4001lem4  15075  4001prm  15076  odrngstr  15264  imasvalstr  15310  ipostr  16351  gsumws1  16575  psgnunilem2  17088  psgnunilem3  17089  oddvdsnn0  17138  pgp0  17189  sylow1lem1  17191  cyggex2  17472  telgsums  17564  srgbinomlem3  17716  srgbinomlem4  17717  srgbinom  17719  snifpsrbag  18531  fczpsrbag  18532  psrlidm  18568  mvrf1  18590  mplcoe3  18631  mplcoe5  18633  ltbwe  18637  psrbag0  18658  psrbagsn  18659  evlslem1  18679  00ply1bas  18774  ply1plusgfvi  18776  coe1sclmul  18816  coe1sclmul2  18818  coe1scl  18821  ply1sclid  18822  ply1idvr1  18827  cply1coe0bi  18835  cnfldstr  18913  nn0subm  18964  expmhm  18976  nn0srg  18977  znf1o  19059  zzngim  19060  cygznlem1  19074  cygznlem2a  19075  cygznlem3  19077  cygth  19079  thlle  19197  cpm2mf  19713  m2cpminvid2lem  19715  m2cpminvid2  19716  m2cpmfo  19717  decpmatid  19731  pmatcollpw3  19745  pmatcollpw3fi1lem1  19747  pmatcollpwscmatlem1  19750  pmatcollpwscmatlem2  19751  idpm2idmp  19762  chfacfscmulgsum  19821  chfacfpmmulgsum  19825  cpmadugsumlemF  19837  dscmet  21524  itgcnlem  22654  dvn0  22785  dvn1  22787  cpncn  22797  dveflem  22838  c1lip2  22857  tdeglem4  22916  deg1le0  22967  ply1divex  22994  ply1rem  23021  fta1g  23025  plyconst  23067  plypf1  23073  plyco  23102  0dgr  23106  0dgrb  23107  coefv0  23109  dgreq0  23126  vieta1lem2  23171  vieta1  23172  aareccl  23186  aannenlem2  23189  taylthlem1  23232  radcnv0  23275  abelthlem6  23295  abelthlem9  23299  logtayl  23509  cxp0  23519  cxpeq  23601  leibpilem2  23771  leibpi  23772  log2ublem3  23778  log2ub  23779  log2le1  23780  birthday  23784  divsqrtsumlem  23809  dmgmn0  23855  lgambdd  23866  sqff1o  24011  ppiublem2  24033  chtublem  24041  bclbnd  24110  bpos1  24113  bposlem8  24121  lgsval  24130  dchrisum0flblem1  24248  dchrisum0flb  24250  ostth2lem2  24374  usgraex0elv  25010  usgrafisbase  25028  wlkonwlk  25151  3v3e3cycl1  25258  4cycl4v4e  25280  4cycl4dv  25281  wwlkn0  25303  wwlkn0s  25319  clwwlkn0  25388  clwwlkf1  25410  erclwwlkref  25427  0egra0rgra  25550  rusgranumwlkb0  25567  rusgra0edg  25569  eupa0  25588  konigsberg  25601  1kp2ke3k  25782  nn0min  28263  lmatcl  28522  lmat22e12  28525  lmat22e21  28526  fsumcvg4  28636  oddpwdc  29054  eulerpartlems  29060  eulerpartlemb  29068  eulerpartlemt  29071  eulerpartgbij  29072  eulerpartlemmf  29075  eulerpartlemgf  29079  eulerpartlemgs2  29080  eulerpartlemn  29081  fib0  29099  fib1  29100  fibp1  29101  ofs1  29260  ofcs1  29261  signsply0  29269  signsvvf  29297  subfac0  29729  subfacval2  29739  subfaclim  29740  cvmliftlem7  29843  cvmliftlem13  29848  bccolsum  30203  fwddifn0  30757  heiborlem4  31894  heiborlem10  31900  nacsfix  35307  diophrw  35354  pell1qr1  35471  monotoddzzfi  35544  jm2.23  35605  hbtlem5  35741  mncn0  35752  aaitgo  35775  mon1pid  35829  brfvrcld  35970  corclrcl  35986  dfrtrcl3  36012  fvrtrcllb0d  36014  fvrtrcllb0da  36015  corcltrcl  36018  cotrclrcl  36021  bccn0  36377  bccn1  36378  binomcxplemradcnv  36386  binomcxplemnotnn0  36390  dvnmul  37435  dvnprodlem3  37440  wallispilem2  37545  wallispi2lem2  37551  stirlinglem5  37557  stirlinglem7  37559  fourierdlem83  37669  fourierdlem112  37698  fouriersw  37711  elaa2lem  37713  elaa2  37714  etransclem48  37762  etransc  37763  iccelpart  38194  bits0ALTV  38255  tgoldbachlt  38356  tgoldbach  38358  pfx2  38400  usgra2pthlem1  38480  uhgrepe  38505  usgo0fis  38565  usgo0fisALT  38566  ssnn0ssfz  38947  nn0o  39147  dig1  39237  0dig2nn0e  39241  0dig2nn0o  39242