Theorem 0nn0 10597

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 2443	. 2 |- 0 = 0
2		elnn0 10584	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 206	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 395	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 368   = wceq 1369   e. wcel 1756   0cc0 9285   NNcn 10325   NN0cn0 10582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-mulcl 9347  ax-i2m1 9353

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-un 3336  df-sn 3881  df-n0 10583

This theorem is referenced by:  nn0ind-raph  10745  numlti  10782  nummul1c  10794  decaddc2  10801  decaddi  10802  decaddci  10803  decaddci2  10804  6p5e11  10808  7p4e11  10810  8p3e11  10814  9p2e11  10820  10p10e20  10828  0elfz  11486  4fvwrd4  11536  injresinjlem  11641  exple1  11926  nn0opth2  12053  faclbnd4lem3  12074  bc0k  12090  bcn1  12092  bccl  12101  hasheq0  12134  hashrabrsn  12140  hashbc  12209  brfi1uzind  12222  brfi1ind  12223  iswrdi  12242  s1fv  12301  2swrdeqwrdeq  12350  wrdeqs1cat  12372  splfv2a  12401  repsw0  12418  0csh0  12433  repswcshw  12449  cshw1  12459  s2fv0  12515  s3fv0  12518  fsumnn0cl  13216  binom  13296  bcxmas  13301  isumnn0nn  13308  climcndslem1  13315  geoser  13332  geomulcvg  13339  ef0lem  13367  ege2le3  13378  ef4p  13400  efgt1p2  13401  efgt1p  13402  ruclem11  13525  nthruz  13537  ndvdssub  13614  bits0  13627  0bits  13638  sadcf  13652  sadc0  13653  sadcaddlem  13656  sadcadd  13657  sadadd2lem  13658  sadadd2  13659  smupf  13677  smup0  13678  smumullem  13691  gcdcl  13704  nn0seqcvgd  13748  algcvg  13754  eucalg  13765  pclem  13908  pcfac  13964  vdwap0  14040  vdwap1  14041  vdwlem6  14050  hashbc0  14069  0ram  14084  0ramcl  14087  ramz2  14088  ramz  14089  ramcl  14093  dec5dvds2  14097  2exp16  14120  11prm  14145  37prm  14151  43prm  14152  83prm  14153  139prm  14154  163prm  14155  317prm  14156  631prm  14157  1259lem1  14158  1259lem2  14159  1259lem3  14160  1259lem4  14161  1259lem5  14162  2503lem1  14164  2503lem2  14165  2503lem3  14166  2503prm  14167  4001lem1  14168  4001lem2  14169  4001lem3  14170  4001lem4  14171  4001prm  14172  odrngstr  14348  imasvalstr  14393  ipostr  15326  gsumws1  15520  psgnunilem2  16004  psgnunilem3  16005  oddvdsnn0  16050  pgp0  16098  sylow1lem1  16100  cyggex2  16376  srgbinomlem3  16643  srgbinomlem4  16644  srgbinom  16646  snifpsrbag  17436  fczpsrbag  17437  psrbasOLD  17452  psrlidm  17477  psrlidmOLD  17478  psrridmOLD  17480  mvridlemOLD  17495  mvrf1  17501  mplcoe3  17548  mplcoe3OLD  17549  mplcoe5  17551  mplcoe2OLD  17553  ltbwe  17557  psrbag0  17579  psrbagsn  17580  evlslem1  17604  00ply1bas  17698  ply1plusgfvi  17700  coe1sclmul  17738  coe1sclmul2  17740  coe1scl  17742  ply1sclid  17743  cnfldstr  17823  nn0subm  17871  expmhm  17883  nn0srg  17884  znf1o  17987  zzngim  17988  cygznlem1  18002  cygznlem2a  18003  cygznlem3  18005  cygth  18007  thlle  18125  dscmet  20168  itgcnlem  21270  dvn0  21401  dvn1  21403  cpncn  21413  dveflem  21454  c1lip2  21473  tdeglem4  21532  deg1le0  21586  ply1divex  21611  ply1rem  21638  fta1g  21642  plyconst  21677  plypf1  21683  plyco  21712  0dgr  21716  0dgrb  21717  coefv0  21718  dgreq0  21735  vieta1lem2  21780  vieta1  21781  aareccl  21795  aannenlem2  21798  taylthlem1  21841  radcnv0  21884  abelthlem6  21904  abelthlem9  21908  logtayl  22108  cxp0  22118  cxpeq  22198  leibpilem2  22339  leibpi  22340  log2ublem3  22346  log2ub  22347  birthday  22351  divsqrsumlem  22376  sqff1o  22523  ppiublem2  22545  chtublem  22553  bclbnd  22622  bpos1  22625  bposlem8  22633  lgsval  22642  dchrisum0flblem1  22760  dchrisum0flb  22762  ostth2lem2  22886  usgraex0elv  23317  usgrafisbase  23330  wlkonwlk  23437  cyclnspth  23520  cyclispthon  23522  3v3e3cycl1  23533  4cycl4v4e  23555  4cycl4dv  23556  eupa0  23598  konigsberg  23611  1kp2ke3k  23656  nn0min  26093  fsumcvg4  26383  nexple  26451  log2le1  26469  oddpwdc  26740  eulerpartlems  26746  eulerpartlemb  26754  eulerpartlemt  26757  eulerpartgbij  26758  eulerpartlemmf  26761  eulerpartlemgf  26765  eulerpartlemgs2  26766  eulerpartlemn  26767  fib0  26785  fib1  26786  fibp1  26787  ofs1  26946  ofcs1  26947  signsply0  26955  signsvvf  26983  dmgmn0  27015  lgambdd  27026  subfac0  27068  subfacval2  27078  subfaclim  27079  cvmliftlem7  27183  cvmliftlem13  27188  relexp0  27334  relexp1  27336  rtrclreclem.refl  27349  risefac0  27533  fallfac0  27534  risefac1  27539  fallfac1  27540  binomfallfaclem2  27546  binomfallfac  27547  bpoly0  28196  bpoly2  28203  bpoly3  28204  bpoly4  28205  fsumcube  28206  heiborlem4  28716  heiborlem10  28722  nacsfix  29051  diophrw  29100  pell1qr1  29215  monotoddzzfi  29286  jm2.23  29348  hbtlem5  29487  mncn0  29499  aaitgo  29522  mon1pid  29576  wallispilem2  29864  wallispi2lem2  29870  stirlinglem5  29876  stirlinglem7  29878  ccat2s1fst  30275  usgra2pthlem1  30303  wwlkn0  30326  wwlkn0s  30342  clwwlkn0  30440  clwwlkf1  30461  erclwwlkref  30486  0egra0rgra  30552  rusgranumwlkb0  30574  rusgra0edg  30576  ssnn0ssfz  30744  ssnn0fi  30749  fsuppmapnn0fiubex  30803  telescgsum  30814  ply1idvr1  30830  pmatcollpw1id  30902  idpmattoidmply1  30918