Theorem 0nn0 11307

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 2622	. 2 |- 0 = 0
2		elnn0 11294	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 218	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 410	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 383   = wceq 1483   e. wcel 1990   0cc0 9936   NNcn 11020   NN0cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-i2m1 10004

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-n0 11293

This theorem is referenced by:  0xnn0  11369  nn0ind-raph  11477  10nn0  11516  declei  11542  numlti  11545  nummul1c  11562  decaddc2OLD  11574  decaddc2  11575  decrmanc  11576  decrmac  11577  decaddm10  11578  decaddi  11579  decaddci  11580  decaddci2  11581  decaddci2OLD  11582  decmul1  11585  decmul1OLD  11586  decmulnc  11591  6p5e11  11600  6p5e11OLD  11601  7p4e11  11605  7p4e11OLD  11606  8p3e11  11612  8p3e11OLD  11613  9p2e11  11619  9p2e11OLD  11620  10p10e20  11628  10p10e20OLD  11629  xnn0n0n1ge2b  11965  0elfz  12436  4fvwrd4  12459  fvinim0ffz  12587  ssnn0fi  12784  fsuppmapnn0fiubex  12792  exple1  12920  sq10  13048  nn0opth2  13059  faclbnd4lem3  13082  bc0k  13098  bcn1  13100  bccl  13109  hasheq0  13154  hashrabrsn  13161  hashbc  13237  fi1uzind  13279  brfi1ind  13281  opfi1ind  13284  fi1uzindOLD  13285  brfi1indOLD  13287  opfi1indOLD  13290  iswrdi  13309  s1fv  13390  ccat2s1fst  13416  2swrdeqwrdeq  13453  wrdeqs1cat  13474  splfv2a  13507  repsw0  13524  0csh0  13539  repswcshw  13558  cshw1  13568  s2fv0  13632  s3fv0  13636  s4fv0  13640  ofs1  13709  relexp0g  13762  relexpaddg  13793  rtrclreclem1  13798  fsumnn0cl  14467  binom  14562  bcxmas  14567  isumnn0nn  14574  climcndslem1  14581  geoser  14599  geomulcvg  14607  risefac0  14758  fallfac0  14759  risefac1  14764  fallfac1  14765  binomfallfaclem2  14771  binomfallfac  14772  bpoly0  14781  bpoly2  14788  bpoly3  14789  bpoly4  14790  fsumcube  14791  ef0lem  14809  ege2le3  14820  ef4p  14843  efgt1p2  14844  efgt1p  14845  ruclem11  14969  nthruz  14982  nn0o  15099  ndvdssub  15133  bits0  15150  0bits  15161  sadcf  15175  sadc0  15176  sadcaddlem  15179  sadcadd  15180  sadadd2lem  15181  sadadd2  15182  smupf  15200  smup0  15201  smumullem  15214  gcdcl  15228  nn0seqcvgd  15283  algcvg  15289  eucalg  15300  lcmcl  15314  lcmfval  15334  lcmfcl  15341  pclem  15543  pcfac  15603  vdwap0  15680  vdwap1  15681  vdwlem6  15690  hashbc0  15709  0ram  15724  0ramcl  15727  ramz2  15728  ramz  15729  ramcl  15733  prmo0  15740  dec5dvds2  15769  2exp16  15797  11prm  15822  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  odrngstr  16066  imasvalstr  16112  ipostr  17153  gsumws1  17376  psgnunilem2  17915  psgnunilem3  17916  oddvdsnn0  17963  pgp0  18011  sylow1lem1  18013  cyggex2  18298  telgsums  18390  srgbinomlem3  18542  srgbinomlem4  18543  srgbinom  18545  snifpsrbag  19366  fczpsrbag  19367  psrlidm  19403  mvrf1  19425  mplcoe3  19466  mplcoe5  19468  ltbwe  19472  psrbag0  19494  psrbagsn  19495  evlslem1  19515  00ply1bas  19610  ply1plusgfvi  19612  coe1sclmul  19652  coe1sclmul2  19654  coe1scl  19657  ply1sclid  19658  ply1idvr1  19663  cply1coe0bi  19670  cnfldstr  19748  cnfldfun  19758  nn0subm  19801  expmhm  19815  nn0srg  19816  znf1o  19900  zzngim  19901  cygznlem1  19915  cygznlem2a  19916  cygznlem3  19918  cygth  19920  thlle  20041  cpm2mf  20557  m2cpminvid2lem  20559  m2cpminvid2  20560  m2cpmfo  20561  decpmatid  20575  pmatcollpw3  20589  pmatcollpw3fi1lem1  20591  pmatcollpwscmatlem1  20594  pmatcollpwscmatlem2  20595  idpm2idmp  20606  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  cpmadugsumlemF  20681  dscmet  22377  itgcnlem  23556  dvn0  23687  dvn1  23689  cpncn  23699  dveflem  23742  c1lip2  23761  tdeglem4  23820  deg1le0  23871  ply1divex  23896  ply1rem  23923  fta1g  23927  plyconst  23962  plypf1  23968  plyco  23997  0dgr  24001  0dgrb  24002  coefv0  24004  dgreq0  24021  vieta1lem2  24066  vieta1  24067  aareccl  24081  aannenlem2  24084  taylthlem1  24127  radcnv0  24170  abelthlem6  24190  abelthlem9  24194  logtayl  24406  cxp0  24416  cxpeq  24498  leibpilem2  24668  leibpi  24669  log2ublem3  24675  log2ub  24676  log2le1  24677  birthday  24681  divsqrtsumlem  24706  dmgmn0  24752  lgambdd  24763  sqff1o  24908  ppiublem2  24928  chtublem  24936  bclbnd  25005  bposlem8  25016  lgsval  25026  dchrisum0flblem1  25197  dchrisum0flb  25199  ostth2lem2  25323  usgrexmplef  26151  usgr0edg0rusgr  26471  usgr2pthlem  26659  wwlksn0s  26746  rusgrnumwwlkb0  26866  clwwlksf1  26917  erclwwlksref  26934  0wlkonlem1  26979  upgr4cycl4dv4e  27045  1kp2ke3k  27303  ex-fac  27308  ex-prmo  27316  nn0min  29567  dpmul1000  29607  dp0h  29610  dpexpp1  29616  dpmul4  29622  threehalves  29623  1mhdrd  29624  lmatcl  29882  lmat22e12  29885  lmat22e21  29886  fsumcvg4  29996  oddpwdc  30416  eulerpartlems  30422  eulerpartlemb  30430  eulerpartlemt  30433  eulerpartgbij  30434  eulerpartlemmf  30437  eulerpartlemgf  30441  eulerpartlemgs2  30442  eulerpartlemn  30443  fib0  30461  fib1  30462  fibp1  30463  ofcs1  30621  signsply0  30628  signsvvf  30656  prodfzo03  30681  repr0  30689  breprexp  30711  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  tgoldbachgtde  30738  subfac0  31159  subfacval2  31169  subfaclim  31170  cvmliftlem7  31273  cvmliftlem13  31278  bccolsum  31625  fwddifn0  32271  heiborlem4  33613  heiborlem10  33619  nacsfix  37275  diophrw  37322  pell1qr1  37435  monotoddzzfi  37507  jm2.23  37563  hbtlem5  37698  mncn0  37709  aaitgo  37732  mon1pid  37783  brfvrcld  37983  corclrcl  37999  dfrtrcl3  38025  fvrtrcllb0d  38027  fvrtrcllb0da  38028  corcltrcl  38031  cotrclrcl  38034  k0004val0  38452  bccn0  38542  bccn1  38543  binomcxplemradcnv  38551  binomcxplemnotnn0  38555  dvnmul  40158  dvnprodlem3  40163  wallispilem2  40283  wallispi2lem2  40289  stirlinglem5  40295  stirlinglem7  40297  fourierdlem83  40406  fourierdlem112  40435  fouriersw  40448  elaa2lem  40450  elaa2  40451  etransclem48  40499  etransc  40500  iccelpart  41369  pfx2  41412  fmtno0  41452  fmtnorec2  41455  fmtno5lem1  41465  fmtno5lem2  41466  fmtno5lem4  41468  257prm  41473  fmtnofac2  41481  fmtnofac1  41482  fmtno4prmfac  41484  fmtno4nprmfac193  41486  fmtno5faclem1  41491  fmtno5faclem2  41492  fmtno5faclem3  41493  fmtno5fac  41494  fmtno5nprm  41495  139prmALT  41511  31prm  41512  127prm  41515  2exp11  41517  m11nprm  41518  bits0ALTV  41590  evengpoap3  41687  tgoldbachlt  41704  tgoldbach  41705  tgoldbachltOLD  41710  tgoldbachOLD  41712  ssnn0ssfz  42127  dig1  42402  0dig2nn0e  42406  0dig2nn0o  42407