Theorem 0nn0 12248

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 2738	. 2 ⊢ 0 = 0
2		elnn0 12235	. . . 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 1539   ∈ wcel 2106  0cc0 10871  ℕcn 11973  ℕ₀cn0 12233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-i2m1 10939

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-n0 12234

This theorem is referenced by:  0xnn0  12311  nn0ind-raph  12420  10nn0  12455  declei  12473  numlti  12474  nummul1c  12486  decaddc2  12493  decrmanc  12494  decrmac  12495  decaddm10  12496  decaddi  12497  decaddci  12498  decaddci2  12499  decmul1  12501  decmulnc  12504  6p5e11  12510  7p4e11  12513  8p3e11  12518  9p2e11  12524  10p10e20  12532  xnn0n0n1ge2b  12867  0elfz  13353  4fvwrd4  13376  fvinim0ffz  13506  ssnn0fi  13705  fsuppmapnn0fiubex  13712  exple1  13894  nn0opth2  13986  faclbnd4lem3  14009  bc0k  14025  bcn1  14027  bccl  14036  hasheq0  14078  hashrabrsn  14087  hashbc  14165  fi1uzind  14211  brfi1ind  14213  opfi1ind  14216  iswrdi  14221  wrdnfi  14251  s1fv  14315  ccat2s1fst  14351  ccat2s1fstOLD  14352  splfv2a  14469  repsw0  14490  0csh0  14506  cshw1  14535  s2fv0  14600  s3fv0  14604  s4fv0  14608  pfx2  14660  ofs1  14681  relexp0g  14733  relexpaddg  14764  rtrclreclem2  14770  fsumnn0cl  15448  binom  15542  bcxmas  15547  isumnn0nn  15554  climcndslem1  15561  geoser  15579  geomulcvg  15588  risefac0  15737  fallfac0  15738  risefac1  15743  fallfac1  15744  binomfallfaclem2  15750  binomfallfac  15751  bpoly0  15760  bpoly2  15767  bpoly3  15768  bpoly4  15769  fsumcube  15770  ef0lem  15788  ege2le3  15799  ef4p  15822  efgt1p2  15823  efgt1p  15824  ruclem11  15949  nthruz  15962  nn0o  16092  ndvdssub  16118  bits0  16135  0bits  16146  sadcf  16160  sadc0  16161  sadcaddlem  16164  sadcadd  16165  sadadd2lem  16166  sadadd2  16167  smupf  16185  smup0  16186  smumullem  16199  gcdcl  16213  nn0seqcvgd  16275  algcvg  16281  eucalg  16292  lcmcl  16306  lcmfval  16326  lcmfcl  16333  pclem  16539  pcfac  16600  vdwap0  16677  vdwap1  16678  vdwlem6  16687  hashbc0  16706  0ram  16721  0ramcl  16724  ramz2  16725  ramz  16726  ramcl  16730  prmo0  16737  dec5dvds2  16766  2exp11  16791  2exp16  16792  11prm  16816  37prm  16822  43prm  16823  83prm  16824  139prm  16825  163prm  16826  317prm  16827  631prm  16828  1259lem1  16832  1259lem2  16833  1259lem3  16834  1259lem4  16835  1259lem5  16836  2503lem1  16838  2503lem2  16839  2503lem3  16840  2503prm  16841  4001lem1  16842  4001lem2  16843  4001lem3  16844  4001lem4  16845  4001prm  16846  plendxnocndx  17094  slotsdifdsndx  17104  slotsdifunifndx  17111  odrngstr  17113  slotsdifplendx2  17127  imasvalstr  17162  ipostr  18247  gsumws1  18476  cycsubm  18821  psgnunilem2  19103  psgnunilem3  19104  odfval  19140  oddvdsnn0  19152  pgp0  19201  sylow1lem1  19203  cyggex2  19498  telgsums  19594  srgbinomlem3  19778  srgbinomlem4  19779  srgbinom  19781  cnfldstr  20599  cnfldfunALTOLD  20611  nn0subm  20653  expmhm  20667  nn0srg  20668  znf1o  20759  zzngim  20760  cygznlem1  20774  cygznlem2a  20775  cygznlem3  20777  cygth  20779  thlleOLD  20904  snifpsrbag  21125  fczpsrbag  21126  psrbagaddcl  21131  psrlidm  21172  mvrf1  21194  mplcoe3  21239  mplcoe5  21241  ltbwe  21245  psrbag0  21270  psrbagsn  21271  evlslem1  21292  mhpsclcl  21337  mhpmulcl  21339  00ply1bas  21411  ply1plusgfvi  21413  coe1sclmul  21453  coe1sclmul2  21455  coe1scl  21458  ply1sclid  21459  ply1idvr1  21464  cply1coe0bi  21471  cpm2mf  21901  m2cpminvid2lem  21903  m2cpminvid2  21904  m2cpmfo  21905  decpmatid  21919  pmatcollpw3  21933  pmatcollpw3fi1lem1  21935  pmatcollpwscmatlem1  21938  pmatcollpwscmatlem2  21939  idpm2idmp  21950  chfacfscmulgsum  22009  chfacfpmmulgsum  22013  cpmadugsumlemF  22025  dscmet  23728  ehl0base  24580  ehl0  24581  itgcnlem  24954  dvn0  25088  dvn1  25090  cpncn  25100  dveflem  25143  c1lip2  25162  tdeglem4OLD  25225  deg1le0  25276  ply1divex  25301  ply1rem  25328  fta1g  25332  plyconst  25367  plypf1  25373  plyco  25402  0dgr  25406  0dgrb  25407  coefv0  25409  dgreq0  25426  vieta1lem2  25471  vieta1  25472  aareccl  25486  aannenlem2  25489  taylthlem1  25532  radcnv0  25575  abelthlem6  25595  abelthlem9  25599  logtayl  25815  cxp0  25825  cxpeq  25910  leibpilem2  26091  leibpi  26092  log2ublem3  26098  log2ub  26099  log2le1  26100  divsqrtsumlem  26129  dmgmn0  26175  lgambdd  26186  sqff1o  26331  ppiublem2  26351  chtublem  26359  bclbnd  26428  bposlem8  26439  lgsval  26449  dchrisum0flblem1  26656  dchrisum0flb  26658  ostth2lem2  26782  usgrexmplef  27626  usgr0edg0rusgr  27942  usgr2pthlem  28131  wwlksn0s  28226  rusgrnumwwlkb0  28336  erclwwlkref  28384  clwwlkf1  28413  0wlkonlem1  28482  upgr4cycl4dv4e  28549  1kp2ke3k  28810  ex-fac  28815  ex-prmo  28823  nn0min  31134  dpmul1000  31173  dp0h  31176  dpexpp1  31182  dpmul4  31188  threehalves  31189  1mhdrd  31190  s1f1  31217  s2f1  31219  cshw1s2  31232  cycpm2tr  31386  freshmansdream  31484  ply1scleq  31668  lmatcl  31766  lmat22e12  31769  lmat22e21  31770  fsumcvg4  31900  oddpwdc  32321  eulerpartlems  32327  eulerpartlemb  32335  eulerpartlemt  32338  eulerpartgbij  32339  eulerpartlemmf  32342  eulerpartlemgf  32346  eulerpartlemgs2  32347  eulerpartlemn  32348  fib0  32366  fib1  32367  fibp1  32368  ofcs1  32523  signsply0  32530  signsvvf  32558  prodfzo03  32583  repr0  32591  breprexp  32613  hgt750lemd  32628  hgt750lem  32631  hgt750lem2  32632  hgt750leme  32638  tgoldbachgtde  32640  0nn0m1nnn0  33071  f1resfz0f1d  33072  usgrgt2cycl  33092  subfac0  33139  subfacval2  33149  subfaclim  33150  cvmliftlem7  33253  cvmliftlem13  33258  bccolsum  33705  fwddifn0  34466  heiborlem4  35972  heiborlem10  35978  12gcd5e1  40011  60gcd6e6  40012  60gcd7e1  40013  420gcd8e4  40014  12lcm5e60  40016  60lcm7e420  40018  420lcm8e840  40019  lcmineqlem  40060  3exp7  40061  3lexlogpow5ineq1  40062  3lexlogpow5ineq2  40063  3lexlogpow5ineq5  40068  aks4d1p1  40084  sticksstones11  40112  sticksstones22  40124  mhphflem  40284  sqn5i  40313  decpmul  40316  sqdeccom12  40317  sq3deccom12  40318  235t711  40319  ex-decpmul  40320  0prjspn  40465  prjcrv0  40470  nacsfix  40534  diophrw  40581  pell1qr1  40693  monotoddzzfi  40764  jm2.23  40818  hbtlem5  40953  mncn0  40964  aaitgo  40987  mon1pid  41030  brfvrcld  41299  corclrcl  41315  dfrtrcl3  41341  fvrtrcllb0d  41343  fvrtrcllb0da  41344  corcltrcl  41347  cotrclrcl  41350  k0004val0  41764  bccn0  41961  bccn1  41962  binomcxplemradcnv  41970  binomcxplemnotnn0  41974  dvnmul  43484  dvnprodlem3  43489  wallispilem2  43607  wallispi2lem2  43613  stirlinglem5  43619  stirlinglem7  43621  fourierdlem83  43730  fourierdlem112  43759  fouriersw  43772  elaa2lem  43774  elaa2  43775  etransclem48  43823  etransc  43824  iccelpart  44885  fmtno0  44992  fmtnorec2  44995  fmtno5lem1  45005  fmtno5lem2  45006  fmtno5lem4  45008  257prm  45013  fmtnofac2  45021  fmtnofac1  45022  fmtno4prmfac  45024  fmtno4nprmfac193  45026  fmtno5faclem1  45031  fmtno5faclem2  45032  fmtno5faclem3  45033  fmtno5fac  45034  fmtno5nprm  45035  139prmALT  45048  31prm  45049  127prm  45051  m11nprm  45053  bits0ALTV  45131  2exp340mod341  45185  nfermltl2rev  45195  evengpoap3  45251  tgoldbachlt  45268  tgoldbach  45269  nn0mnd  45373  ssnn0ssfz  45685  dig1  45954  0dig2nn0e  45958  0dig2nn0o  45959  0aryfvalel  45980  itcoval0  46008  itcoval1  46009  ackval0  46026  ackval1  46027  ackvalsuc0val  46033  ackval0012  46035  ackval1012  46036  ackval2012  46037  ackval3012  46038  ackval41a  46040  prstclevalOLD  46350