Theorem 0nn0 12350

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
0nn0	⊢ 0 ∈ ℕ0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2736	. 2 ⊢ 0 = 0
2		elnn0 12337	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 227	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 873	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 844   = wceq 1540   ∈ wcel 2105  0cc0 10973  ℕcn 12075  ℕ₀cn0 12335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-mulcl 11035  ax-i2m1 11041

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-un 3903  df-sn 4575  df-n0 12336

This theorem is referenced by:  0xnn0  12413  nn0ind-raph  12522  10nn0  12557  declei  12575  numlti  12576  nummul1c  12588  decaddc2  12595  decrmanc  12596  decrmac  12597  decaddm10  12598  decaddi  12599  decaddci  12600  decaddci2  12601  decmul1  12603  decmulnc  12606  6p5e11  12612  7p4e11  12615  8p3e11  12620  9p2e11  12626  10p10e20  12634  xnn0n0n1ge2b  12969  0elfz  13455  4fvwrd4  13478  fvinim0ffz  13608  ssnn0fi  13807  fsuppmapnn0fiubex  13814  exple1  13996  nn0opth2  14088  faclbnd4lem3  14111  bc0k  14127  bcn1  14129  bccl  14138  hasheq0  14179  hashrabrsn  14188  hashbc  14266  fi1uzind  14312  brfi1ind  14314  opfi1ind  14317  iswrdi  14322  wrdnfi  14352  s1fv  14415  ccat2s1fst  14450  ccat2s1fstOLD  14451  splfv2a  14568  repsw0  14589  0csh0  14605  cshw1  14634  s2fv0  14700  s3fv0  14704  s4fv0  14708  pfx2  14760  ofs1  14781  relexp0g  14833  relexpaddg  14864  rtrclreclem2  14870  fsumnn0cl  15548  binom  15642  bcxmas  15647  isumnn0nn  15654  climcndslem1  15661  geoser  15679  geomulcvg  15688  risefac0  15837  fallfac0  15838  risefac1  15843  fallfac1  15844  binomfallfaclem2  15850  binomfallfac  15851  bpoly0  15860  bpoly2  15867  bpoly3  15868  bpoly4  15869  fsumcube  15870  ef0lem  15888  ege2le3  15899  ef4p  15922  efgt1p2  15923  efgt1p  15924  ruclem11  16049  nthruz  16062  nn0o  16192  ndvdssub  16218  bits0  16235  0bits  16246  sadcf  16260  sadc0  16261  sadcaddlem  16264  sadcadd  16265  sadadd2lem  16266  sadadd2  16267  smupf  16285  smup0  16286  smumullem  16299  gcdcl  16313  nn0seqcvgd  16373  algcvg  16379  eucalg  16390  lcmcl  16404  lcmfval  16424  lcmfcl  16431  pclem  16637  pcfac  16698  vdwap0  16775  vdwap1  16776  vdwlem6  16785  hashbc0  16804  0ram  16819  0ramcl  16822  ramz2  16823  ramz  16824  ramcl  16828  prmo0  16835  dec5dvds2  16864  2exp11  16889  2exp16  16890  11prm  16914  37prm  16920  43prm  16921  83prm  16922  139prm  16923  163prm  16924  317prm  16925  631prm  16926  1259lem1  16930  1259lem2  16931  1259lem3  16932  1259lem4  16933  1259lem5  16934  2503lem1  16936  2503lem2  16937  2503lem3  16938  2503prm  16939  4001lem1  16940  4001lem2  16941  4001lem3  16942  4001lem4  16943  4001prm  16944  plendxnocndx  17192  slotsdifdsndx  17202  slotsdifunifndx  17209  odrngstr  17211  slotsdifplendx2  17225  imasvalstr  17260  ipostr  18345  gsumws1  18574  cycsubm  18918  psgnunilem2  19200  psgnunilem3  19201  odfval  19237  oddvdsnn0  19249  pgp0  19298  sylow1lem1  19300  cyggex2  19594  telgsums  19690  srgbinomlem3  19874  srgbinomlem4  19875  srgbinom  19877  cnfldstr  20706  cnfldfunALTOLD  20718  nn0subm  20760  expmhm  20774  nn0srg  20775  znf1o  20866  zzngim  20867  cygznlem1  20881  cygznlem2a  20882  cygznlem3  20884  cygth  20886  thlleOLD  21011  snifpsrbag  21232  fczpsrbag  21233  psrbagaddcl  21238  psrlidm  21279  mvrf1  21301  mplcoe3  21346  mplcoe5  21348  ltbwe  21352  psrbag0  21377  psrbagsn  21378  evlslem1  21399  mhpsclcl  21444  mhpmulcl  21446  00ply1bas  21518  ply1plusgfvi  21520  coe1sclmul  21560  coe1sclmul2  21562  coe1scl  21565  ply1sclid  21566  ply1idvr1  21571  cply1coe0bi  21578  cpm2mf  22008  m2cpminvid2lem  22010  m2cpminvid2  22011  m2cpmfo  22012  decpmatid  22026  pmatcollpw3  22040  pmatcollpw3fi1lem1  22042  pmatcollpwscmatlem1  22045  pmatcollpwscmatlem2  22046  idpm2idmp  22057  chfacfscmulgsum  22116  chfacfpmmulgsum  22120  cpmadugsumlemF  22132  dscmet  23835  ehl0base  24687  ehl0  24688  itgcnlem  25061  dvn0  25195  dvn1  25197  cpncn  25207  dveflem  25250  c1lip2  25269  tdeglem4OLD  25332  deg1le0  25383  ply1divex  25408  ply1rem  25435  fta1g  25439  plyconst  25474  plypf1  25480  plyco  25509  0dgr  25513  0dgrb  25514  coefv0  25516  dgreq0  25533  vieta1lem2  25578  vieta1  25579  aareccl  25593  aannenlem2  25596  taylthlem1  25639  radcnv0  25682  abelthlem6  25702  abelthlem9  25706  logtayl  25922  cxp0  25932  cxpeq  26017  leibpilem2  26198  leibpi  26199  log2ublem3  26205  log2ub  26206  log2le1  26207  divsqrtsumlem  26236  dmgmn0  26282  lgambdd  26293  sqff1o  26438  ppiublem2  26458  chtublem  26466  bclbnd  26535  bposlem8  26546  lgsval  26556  dchrisum0flblem1  26763  dchrisum0flb  26765  ostth2lem2  26889  usgrexmplef  27916  usgr0edg0rusgr  28232  usgr2pthlem  28420  wwlksn0s  28515  rusgrnumwwlkb0  28625  erclwwlkref  28673  clwwlkf1  28702  0wlkonlem1  28771  upgr4cycl4dv4e  28838  1kp2ke3k  29099  ex-fac  29104  ex-prmo  29112  nn0min  31421  dpmul1000  31460  dp0h  31463  dpexpp1  31469  dpmul4  31475  threehalves  31476  1mhdrd  31477  s1f1  31504  s2f1  31506  cshw1s2  31519  cycpm2tr  31673  freshmansdream  31771  ply1scleq  31965  lmatcl  32064  lmat22e12  32067  lmat22e21  32068  fsumcvg4  32198  oddpwdc  32621  eulerpartlems  32627  eulerpartlemb  32635  eulerpartlemt  32638  eulerpartgbij  32639  eulerpartlemmf  32642  eulerpartlemgf  32646  eulerpartlemgs2  32647  eulerpartlemn  32648  fib0  32666  fib1  32667  fibp1  32668  ofcs1  32823  signsply0  32830  signsvvf  32858  prodfzo03  32883  repr0  32891  breprexp  32913  hgt750lemd  32928  hgt750lem  32931  hgt750lem2  32932  hgt750leme  32938  tgoldbachgtde  32940  0nn0m1nnn0  33370  f1resfz0f1d  33371  usgrgt2cycl  33391  subfac0  33438  subfacval2  33448  subfaclim  33449  cvmliftlem7  33552  cvmliftlem13  33557  bccolsum  33997  fwddifn0  34605  heiborlem4  36128  heiborlem10  36134  12gcd5e1  40316  60gcd6e6  40317  60gcd7e1  40318  420gcd8e4  40319  12lcm5e60  40321  60lcm7e420  40323  420lcm8e840  40324  lcmineqlem  40365  3exp7  40366  3lexlogpow5ineq1  40367  3lexlogpow5ineq2  40368  3lexlogpow5ineq5  40373  aks4d1p1  40389  sticksstones11  40420  sticksstones22  40432  mhphflem  40595  sqn5i  40624  decpmul  40627  sqdeccom12  40628  sq3deccom12  40629  235t711  40630  ex-decpmul  40631  0prjspn  40778  nacsfix  40847  diophrw  40894  pell1qr1  41006  monotoddzzfi  41078  jm2.23  41132  hbtlem5  41267  mncn0  41278  aaitgo  41301  mon1pid  41344  brfvrcld  41672  corclrcl  41688  dfrtrcl3  41714  fvrtrcllb0d  41716  fvrtrcllb0da  41717  corcltrcl  41720  cotrclrcl  41723  k0004val0  42137  bccn0  42334  bccn1  42335  binomcxplemradcnv  42343  binomcxplemnotnn0  42347  dvnmul  43872  dvnprodlem3  43877  wallispilem2  43995  wallispi2lem2  44001  stirlinglem5  44007  stirlinglem7  44009  fourierdlem83  44118  fourierdlem112  44147  fouriersw  44160  elaa2lem  44162  elaa2  44163  etransclem48  44211  etransc  44212  iccelpart  45303  fmtno0  45410  fmtnorec2  45413  fmtno5lem1  45423  fmtno5lem2  45424  fmtno5lem4  45426  257prm  45431  fmtnofac2  45439  fmtnofac1  45440  fmtno4prmfac  45442  fmtno4nprmfac193  45444  fmtno5faclem1  45449  fmtno5faclem2  45450  fmtno5faclem3  45451  fmtno5fac  45452  fmtno5nprm  45453  139prmALT  45466  31prm  45467  127prm  45469  m11nprm  45471  bits0ALTV  45549  2exp340mod341  45603  nfermltl2rev  45613  evengpoap3  45669  tgoldbachlt  45686  tgoldbach  45687  nn0mnd  45791  ssnn0ssfz  46103  dig1  46372  0dig2nn0e  46376  0dig2nn0o  46377  0aryfvalel  46398  itcoval0  46426  itcoval1  46427  ackval0  46444  ackval1  46445  ackvalsuc0val  46451  ackval0012  46453  ackval1012  46454  ackval2012  46455  ackval3012  46456  ackval41a  46458  prstclevalOLD  46768