Theorem 0nn0 10799

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 2460	. 2 |- 0 = 0
2		elnn0 10786	. . . 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 1374   e. wcel 1762   0cc0 9481   NNcn 10525   NN0cn0 10784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-i2m1 9549

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-sn 4021  df-n0 10785

This theorem is referenced by:  nn0ind-raph  10950  numlti  10989  nummul1c  11001  decaddc2  11008  decaddi  11009  decaddci  11010  decaddci2  11011  6p5e11  11015  7p4e11  11017  8p3e11  11021  9p2e11  11027  10p10e20  11035  0elfz  11761  4fvwrd4  11779  injresinjlem  11882  ssnn0fi  12050  fsuppmapnn0fiubex  12054  exple1  12180  nn0opth2  12307  faclbnd4lem3  12328  bc0k  12344  bcn1  12346  bccl  12355  hasheq0  12388  hashrabrsn  12395  hashbc  12455  brfi1uzind  12485  brfi1ind  12486  iswrdi  12505  s1fv  12569  ccat2s1fst  12593  2swrdeqwrdeq  12628  wrdeqs1cat  12650  splfv2a  12682  repsw0  12699  0csh0  12714  repswcshw  12730  cshw1  12740  s2fv0  12800  s3fv0  12803  fsumnn0cl  13507  binom  13594  bcxmas  13599  isumnn0nn  13606  climcndslem1  13613  geoser  13630  geomulcvg  13637  ef0lem  13665  ege2le3  13676  ef4p  13698  efgt1p2  13699  efgt1p  13700  ruclem11  13823  nthruz  13835  ndvdssub  13913  bits0  13926  0bits  13937  sadcf  13951  sadc0  13952  sadcaddlem  13955  sadcadd  13956  sadadd2lem  13957  sadadd2  13958  smupf  13976  smup0  13977  smumullem  13990  gcdcl  14003  nn0seqcvgd  14047  algcvg  14053  eucalg  14064  pclem  14210  pcfac  14266  vdwap0  14342  vdwap1  14343  vdwlem6  14352  hashbc0  14371  0ram  14386  0ramcl  14389  ramz2  14390  ramz  14391  ramcl  14395  dec5dvds2  14399  2exp16  14422  11prm  14447  37prm  14453  43prm  14454  83prm  14455  139prm  14456  163prm  14457  317prm  14458  631prm  14459  1259lem1  14460  1259lem2  14461  1259lem3  14462  1259lem4  14463  1259lem5  14464  2503lem1  14466  2503lem2  14467  2503lem3  14468  2503prm  14469  4001lem1  14470  4001lem2  14471  4001lem3  14472  4001lem4  14473  4001prm  14474  odrngstr  14651  imasvalstr  14696  ipostr  15629  gsumws1  15823  psgnunilem2  16309  psgnunilem3  16310  oddvdsnn0  16357  pgp0  16405  sylow1lem1  16407  cyggex2  16683  telgsums  16806  srgbinomlem3  16974  srgbinomlem4  16975  srgbinom  16977  snifpsrbag  17779  fczpsrbag  17780  psrbasOLD  17795  psrlidm  17820  psrlidmOLD  17821  psrridmOLD  17823  mvridlemOLD  17839  mvrf1  17845  mplcoe3  17892  mplcoe3OLD  17893  mplcoe5  17895  mplcoe2OLD  17897  ltbwe  17901  psrbag0  17923  psrbagsn  17924  evlslem1  17948  00ply1bas  18045  ply1plusgfvi  18047  coe1sclmul  18087  coe1sclmul2  18089  coe1scl  18092  ply1sclid  18093  ply1idvr1  18098  cply1coe0bi  18106  cnfldstr  18186  nn0subm  18234  expmhm  18246  nn0srg  18247  znf1o  18350  zzngim  18351  cygznlem1  18365  cygznlem2a  18366  cygznlem3  18368  cygth  18370  thlle  18488  cpm2mf  19013  m2cpminvid2lem  19015  m2cpminvid2  19016  m2cpmfo  19017  decpmatid  19031  pmatcollpw3  19045  pmatcollpw3fi1lem1  19047  pmatcollpwscmatlem1  19050  pmatcollpwscmatlem2  19051  idpm2idmp  19062  chfacfscmulgsum  19121  chfacfpmmulgsum  19125  cpmadugsumlemF  19137  dscmet  20821  itgcnlem  21924  dvn0  22055  dvn1  22057  cpncn  22067  dveflem  22108  c1lip2  22127  tdeglem4  22186  deg1le0  22240  ply1divex  22265  ply1rem  22292  fta1g  22296  plyconst  22331  plypf1  22337  plyco  22366  0dgr  22370  0dgrb  22371  coefv0  22372  dgreq0  22389  vieta1lem2  22434  vieta1  22435  aareccl  22449  aannenlem2  22452  taylthlem1  22495  radcnv0  22538  abelthlem6  22558  abelthlem9  22562  logtayl  22762  cxp0  22772  cxpeq  22852  leibpilem2  22993  leibpi  22994  log2ublem3  23000  log2ub  23001  birthday  23005  divsqrsumlem  23030  sqff1o  23177  ppiublem2  23199  chtublem  23207  bclbnd  23276  bpos1  23279  bposlem8  23287  lgsval  23296  dchrisum0flblem1  23414  dchrisum0flb  23416  ostth2lem2  23540  usgraex0elv  24058  usgrafisbase  24076  wlkonwlk  24199  cyclnspth  24293  cyclispthon  24295  3v3e3cycl1  24306  4cycl4v4e  24328  4cycl4dv  24329  wwlkn0  24351  wwlkn0s  24367  clwwlkn0  24436  clwwlkf1  24458  erclwwlkref  24475  0egra0rgra  24598  rusgranumwlkb0  24615  rusgra0edg  24617  eupa0  24636  konigsberg  24649  1kp2ke3k  24830  nn0min  27265  fsumcvg4  27554  nexple  27631  log2le1  27649  oddpwdc  27919  eulerpartlems  27925  eulerpartlemb  27933  eulerpartlemt  27936  eulerpartgbij  27937  eulerpartlemmf  27940  eulerpartlemgf  27944  eulerpartlemgs2  27945  eulerpartlemn  27946  fib0  27964  fib1  27965  fibp1  27966  ofs1  28125  ofcs1  28126  signsply0  28134  signsvvf  28162  dmgmn0  28194  lgambdd  28205  subfac0  28247  subfacval2  28257  subfaclim  28258  cvmliftlem7  28362  cvmliftlem13  28367  relexp0  28513  relexp1  28515  rtrclreclem.refl  28528  risefac0  28712  fallfac0  28713  risefac1  28718  fallfac1  28719  binomfallfaclem2  28725  binomfallfac  28726  bpoly0  29375  bpoly2  29382  bpoly3  29383  bpoly4  29384  fsumcube  29385  heiborlem4  29900  heiborlem10  29906  nacsfix  30235  diophrw  30283  pell1qr1  30398  monotoddzzfi  30469  jm2.23  30531  hbtlem5  30670  mncn0  30682  aaitgo  30705  mon1pid  30759  wallispilem2  31321  wallispi2lem2  31327  stirlinglem5  31333  stirlinglem7  31335  fourierdlem83  31445  fourierdlem112  31474  fouriersw  31487  usgra2pthlem1  31777  usgo0fis  31834  ssnn0ssfz  31877