Theorem 0nn0 10881

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 2450	. 2 |- 0 = 0
2		elnn0 10868	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 210	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 397	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 370   = wceq 1443   e. wcel 1886   0cc0 9536   NNcn 10606   NN0cn0 10866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-mulcl 9598  ax-i2m1 9604

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-un 3408  df-sn 3968  df-n0 10867

This theorem is referenced by:  nn0ind-raph  11032  numlti  11072  nummul1c  11084  decaddc2  11091  decaddi  11092  decaddci  11093  decaddci2  11094  6p5e11  11098  7p4e11  11100  8p3e11  11104  9p2e11  11110  10p10e20  11118  0elfz  11886  4fvwrd4  11906  ssnn0fi  12194  fsuppmapnn0fiubex  12201  exple1  12329  nn0opth2  12455  faclbnd4lem3  12477  bc0k  12493  bcn1  12495  bccl  12504  hasheq0  12541  hashrabrsn  12548  hashbc  12613  fi1uzind  12647  brfi1ind  12649  opfi1ind  12652  iswrdi  12672  s1fv  12743  ccat2s1fst  12767  2swrdeqwrdeq  12804  wrdeqs1cat  12826  splfv2a  12858  repsw0  12875  0csh0  12890  repswcshw  12906  cshw1  12916  s2fv0  12976  s3fv0  12979  s4fv0  12983  relexp0g  13078  relexpaddg  13109  rtrclreclem1  13114  fsumnn0cl  13795  binom  13881  bcxmas  13886  isumnn0nn  13893  climcndslem1  13900  geoser  13918  geomulcvg  13925  risefac0  14073  fallfac0  14074  risefac1  14079  fallfac1  14080  binomfallfaclem2  14086  binomfallfac  14087  bpoly0  14096  bpoly2  14103  bpoly3  14104  bpoly4  14105  fsumcube  14106  ef0lem  14126  ege2le3  14137  ef4p  14160  efgt1p2  14161  efgt1p  14162  ruclem11  14285  nthruz  14297  ndvdssub  14381  bits0  14394  0bits  14406  sadcf  14420  sadc0  14421  sadcaddlem  14424  sadcadd  14425  sadadd2lem  14426  sadadd2  14427  smupf  14445  smup0  14446  smumullem  14459  gcdcl  14473  nn0seqcvgd  14522  algcvg  14528  eucalg  14539  lcmcl  14559  lcmfval  14584  lcmfvalOLD  14588  lcmfcl  14594  pclem  14781  pcfac  14837  vdwap0  14919  vdwap1  14920  vdwlem6  14929  hashbc0  14950  0ram  14971  0ramcl  14974  ramz2  14975  ramz  14976  ramcl  14980  prmo0  14987  dec5dvds2  15030  2exp16  15054  11prm  15079  37prm  15085  43prm  15086  83prm  15087  139prm  15088  163prm  15089  317prm  15090  631prm  15091  1259lem1  15095  1259lem2  15096  1259lem3  15097  1259lem4  15098  1259lem5  15099  2503lem1  15101  2503lem2  15102  2503lem3  15103  2503prm  15104  4001lem1  15105  4001lem2  15106  4001lem3  15107  4001lem4  15108  4001prm  15109  odrngstr  15297  imasvalstr  15343  ipostr  16392  gsumws1  16616  psgnunilem2  17129  psgnunilem3  17130  oddvdsnn0  17186  pgp0  17241  sylow1lem1  17243  cyggex2  17524  telgsums  17616  srgbinomlem3  17768  srgbinomlem4  17769  srgbinom  17771  snifpsrbag  18583  fczpsrbag  18584  psrlidm  18620  mvrf1  18642  mplcoe3  18683  mplcoe5  18685  ltbwe  18689  psrbag0  18710  psrbagsn  18711  evlslem1  18731  00ply1bas  18826  ply1plusgfvi  18828  coe1sclmul  18868  coe1sclmul2  18870  coe1scl  18873  ply1sclid  18874  ply1idvr1  18879  cply1coe0bi  18887  cnfldstr  18965  nn0subm  19016  expmhm  19029  nn0srg  19030  znf1o  19115  zzngim  19116  cygznlem1  19130  cygznlem2a  19131  cygznlem3  19133  cygth  19135  thlle  19253  cpm2mf  19769  m2cpminvid2lem  19771  m2cpminvid2  19772  m2cpmfo  19773  decpmatid  19787  pmatcollpw3  19801  pmatcollpw3fi1lem1  19803  pmatcollpwscmatlem1  19806  pmatcollpwscmatlem2  19807  idpm2idmp  19818  chfacfscmulgsum  19877  chfacfpmmulgsum  19881  cpmadugsumlemF  19893  dscmet  21580  itgcnlem  22740  dvn0  22871  dvn1  22873  cpncn  22883  dveflem  22924  c1lip2  22943  tdeglem4  23002  deg1le0  23053  ply1divex  23080  ply1rem  23107  fta1g  23111  plyconst  23153  plypf1  23159  plyco  23188  0dgr  23192  0dgrb  23193  coefv0  23195  dgreq0  23212  vieta1lem2  23257  vieta1  23258  aareccl  23275  aannenlem2  23278  taylthlem1  23321  radcnv0  23364  abelthlem6  23384  abelthlem9  23388  logtayl  23598  cxp0  23608  cxpeq  23690  leibpilem2  23860  leibpi  23861  log2ublem3  23867  log2ub  23868  log2le1  23869  birthday  23873  divsqrtsumlem  23898  dmgmn0  23944  lgambdd  23955  sqff1o  24102  ppiublem2  24124  chtublem  24132  bclbnd  24201  bpos1  24204  bposlem8  24212  lgsval  24221  dchrisum0flblem1  24339  dchrisum0flb  24341  ostth2lem2  24465  usgraex0elv  25116  usgrafisbase  25135  wlkonwlk  25258  3v3e3cycl1  25365  4cycl4v4e  25387  4cycl4dv  25388  wwlkn0  25410  wwlkn0s  25426  clwwlkn0  25495  clwwlkf1  25517  erclwwlkref  25534  0egra0rgra  25657  rusgranumwlkb0  25674  rusgra0edg  25676  eupa0  25695  konigsberg  25708  1kp2ke3k  25889  nn0min  28377  lmatcl  28635  lmat22e12  28638  lmat22e21  28639  fsumcvg4  28749  oddpwdc  29180  eulerpartlems  29186  eulerpartlemb  29194  eulerpartlemt  29197  eulerpartgbij  29198  eulerpartlemmf  29201  eulerpartlemgf  29205  eulerpartlemgs2  29206  eulerpartlemn  29207  fib0  29225  fib1  29226  fibp1  29227  ofs1  29424  ofcs1  29425  signsply0  29433  signsvvf  29461  subfac0  29893  subfacval2  29903  subfaclim  29904  cvmliftlem7  30007  cvmliftlem13  30012  bccolsum  30368  fwddifn0  30924  heiborlem4  32139  heiborlem10  32145  nacsfix  35548  diophrw  35595  pell1qr1  35711  monotoddzzfi  35784  jm2.23  35845  hbtlem5  35981  mncn0  35992  aaitgo  36022  mon1pid  36076  brfvrcld  36277  corclrcl  36293  dfrtrcl3  36319  fvrtrcllb0d  36321  fvrtrcllb0da  36322  corcltrcl  36325  cotrclrcl  36328  bccn0  36686  bccn1  36687  binomcxplemradcnv  36695  binomcxplemnotnn0  36699  dvnmul  37812  dvnprodlem3  37817  wallispilem2  37922  wallispi2lem2  37928  stirlinglem5  37934  stirlinglem7  37936  fourierdlem83  38047  fourierdlem112  38076  fouriersw  38089  elaa2lem  38091  elaa2lemOLD  38092  elaa2  38093  etransclem48OLD  38141  etransclem48  38142  etransc  38143  iccelpart  38741  bits0ALTV  38802  tgoldbachlt  38903  tgoldbach  38905  pfx2  38947  0xnn0  39063  usgr0edg0rusgr  39574  wlkOnwlk  39644  0wlkOn  39649  usgra2pthlem1  39654  usgo0fis  39737  usgo0fisALT  39738  ssnn0ssfz  40117  nn0o  40316  dig1  40406  0dig2nn0e  40410  0dig2nn0o  40411