Theorem 0nn0 10816

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 10803	. . . 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 1383   e. wcel 1804   0cc0 9495   NNcn 10542   NN0cn0 10801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-mulcl 9557  ax-i2m1 9563

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-n0 10802

This theorem is referenced by:  nn0ind-raph  10969  numlti  11008  nummul1c  11020  decaddc2  11027  decaddi  11028  decaddci  11029  decaddci2  11030  6p5e11  11034  7p4e11  11036  8p3e11  11040  9p2e11  11046  10p10e20  11054  0elfz  11781  4fvwrd4  11801  ssnn0fi  12073  fsuppmapnn0fiubex  12077  exple1  12204  nn0opth2  12331  faclbnd4lem3  12352  bc0k  12368  bcn1  12370  bccl  12379  hasheq0  12412  hashrabrsn  12419  hashbc  12481  brfi1uzind  12511  brfi1ind  12512  iswrdi  12531  s1fv  12598  ccat2s1fst  12622  2swrdeqwrdeq  12657  wrdeqs1cat  12679  splfv2a  12711  repsw0  12728  0csh0  12743  repswcshw  12759  cshw1  12769  s2fv0  12829  s3fv0  12832  fsumnn0cl  13537  binom  13621  bcxmas  13626  isumnn0nn  13633  climcndslem1  13640  geoser  13657  geomulcvg  13664  ef0lem  13692  ege2le3  13703  ef4p  13725  efgt1p2  13726  efgt1p  13727  ruclem11  13850  nthruz  13862  ndvdssub  13942  bits0  13955  0bits  13966  sadcf  13980  sadc0  13981  sadcaddlem  13984  sadcadd  13985  sadadd2lem  13986  sadadd2  13987  smupf  14005  smup0  14006  smumullem  14019  gcdcl  14032  nn0seqcvgd  14076  algcvg  14082  eucalg  14093  pclem  14239  pcfac  14295  vdwap0  14371  vdwap1  14372  vdwlem6  14381  hashbc0  14400  0ram  14415  0ramcl  14418  ramz2  14419  ramz  14420  ramcl  14424  dec5dvds2  14428  2exp16  14452  11prm  14477  37prm  14483  43prm  14484  83prm  14485  139prm  14486  163prm  14487  317prm  14488  631prm  14489  1259lem1  14490  1259lem2  14491  1259lem3  14492  1259lem4  14493  1259lem5  14494  2503lem1  14496  2503lem2  14497  2503lem3  14498  2503prm  14499  4001lem1  14500  4001lem2  14501  4001lem3  14502  4001lem4  14503  4001prm  14504  odrngstr  14681  imasvalstr  14726  ipostr  15657  gsumws1  15881  psgnunilem2  16394  psgnunilem3  16395  oddvdsnn0  16442  pgp0  16490  sylow1lem1  16492  cyggex2  16773  telgsums  16896  srgbinomlem3  17067  srgbinomlem4  17068  srgbinom  17070  snifpsrbag  17889  fczpsrbag  17890  psrbasOLD  17905  psrlidm  17930  psrlidmOLD  17931  psrridmOLD  17933  mvridlemOLD  17949  mvrf1  17955  mplcoe3  18002  mplcoe3OLD  18003  mplcoe5  18005  mplcoe2OLD  18007  ltbwe  18011  psrbag0  18033  psrbagsn  18034  evlslem1  18058  00ply1bas  18155  ply1plusgfvi  18157  coe1sclmul  18197  coe1sclmul2  18199  coe1scl  18202  ply1sclid  18203  ply1idvr1  18208  cply1coe0bi  18216  cnfldstr  18296  nn0subm  18347  expmhm  18359  nn0srg  18360  znf1o  18463  zzngim  18464  cygznlem1  18478  cygznlem2a  18479  cygznlem3  18481  cygth  18483  thlle  18601  cpm2mf  19126  m2cpminvid2lem  19128  m2cpminvid2  19129  m2cpmfo  19130  decpmatid  19144  pmatcollpw3  19158  pmatcollpw3fi1lem1  19160  pmatcollpwscmatlem1  19163  pmatcollpwscmatlem2  19164  idpm2idmp  19175  chfacfscmulgsum  19234  chfacfpmmulgsum  19238  cpmadugsumlemF  19250  dscmet  20966  itgcnlem  22069  dvn0  22200  dvn1  22202  cpncn  22212  dveflem  22253  c1lip2  22272  tdeglem4  22331  deg1le0  22385  ply1divex  22410  ply1rem  22437  fta1g  22441  plyconst  22476  plypf1  22482  plyco  22511  0dgr  22515  0dgrb  22516  coefv0  22517  dgreq0  22534  vieta1lem2  22579  vieta1  22580  aareccl  22594  aannenlem2  22597  taylthlem1  22640  radcnv0  22683  abelthlem6  22703  abelthlem9  22707  logtayl  22913  cxp0  22923  cxpeq  23003  leibpilem2  23144  leibpi  23145  log2ublem3  23151  log2ub  23152  birthday  23156  divsqrtsumlem  23181  sqff1o  23328  ppiublem2  23350  chtublem  23358  bclbnd  23427  bpos1  23430  bposlem8  23438  lgsval  23447  dchrisum0flblem1  23565  dchrisum0flb  23567  ostth2lem2  23691  usgraex0elv  24268  usgrafisbase  24286  wlkonwlk  24409  3v3e3cycl1  24516  4cycl4v4e  24538  4cycl4dv  24539  wwlkn0  24561  wwlkn0s  24577  clwwlkn0  24646  clwwlkf1  24668  erclwwlkref  24685  0egra0rgra  24808  rusgranumwlkb0  24825  rusgra0edg  24827  eupa0  24846  konigsberg  24859  1kp2ke3k  25039  nn0min  27484  fsumcvg4  27805  log2le1  27896  oddpwdc  28166  eulerpartlems  28172  eulerpartlemb  28180  eulerpartlemt  28183  eulerpartgbij  28184  eulerpartlemmf  28187  eulerpartlemgf  28191  eulerpartlemgs2  28192  eulerpartlemn  28193  fib0  28211  fib1  28212  fibp1  28213  ofs1  28372  ofcs1  28373  signsply0  28381  signsvvf  28409  dmgmn0  28441  lgambdd  28452  subfac0  28494  subfacval2  28504  subfaclim  28505  cvmliftlem7  28609  cvmliftlem13  28614  relexp0  28925  relexp1  28927  rtrclreclem.refl  28940  risefac0  29124  fallfac0  29125  risefac1  29130  fallfac1  29131  binomfallfaclem2  29137  binomfallfac  29138  bpoly0  29787  bpoly2  29794  bpoly3  29795  bpoly4  29796  fsumcube  29797  heiborlem4  30285  heiborlem10  30291  nacsfix  30619  diophrw  30667  pell1qr1  30782  monotoddzzfi  30853  jm2.23  30913  hbtlem5  31052  mncn0  31064  aaitgo  31087  mon1pid  31141  lcmcl  31183  wallispilem2  31737  wallispi2lem2  31743  stirlinglem5  31749  stirlinglem7  31751  fourierdlem83  31861  fourierdlem112  31890  fouriersw  31903  usgra2pthlem1  32191  uhgrepe  32216  usgo0fis  32276  usgo0fisALT  32277  ssnn0ssfz  32671