Theorem 0nn0 12416

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 12403	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 228	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 876	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2113  0cc0 11026  ℕcn 12145  ℕ₀cn0 12401

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-i2m1 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-n0 12402

This theorem is referenced by:  0xnn0  12480  nn0ind-raph  12592  10nn0  12625  declei  12643  numlti  12644  nummul1c  12656  decaddc2  12663  decrmanc  12664  decrmac  12665  decaddm10  12666  decaddi  12667  decaddci  12668  decaddci2  12669  decmul1  12671  decmulnc  12674  6p5e11  12680  7p4e11  12683  8p3e11  12688  9p2e11  12694  10p10e20  12702  xnn0n0n1ge2b  13046  0elfz  13540  4fvwrd4  13564  fvinim0ffz  13705  ssnn0fi  13908  fsuppmapnn0fiubex  13915  exple1  14100  nn0opth2  14195  faclbnd4lem3  14218  bc0k  14234  bcn1  14236  bccl  14245  hasheq0  14286  hashrabrsn  14295  hashbc  14376  fi1uzind  14430  brfi1ind  14432  opfi1ind  14435  iswrdi  14440  wrdnfi  14471  s1fv  14534  ccat2s1fst  14563  splfv2a  14679  repsw0  14700  0csh0  14716  cshw1  14745  s2fv0  14810  s3fv0  14814  s4fv0  14818  pfx2  14870  ofs1  14893  relexp0g  14945  relexpaddg  14976  rtrclreclem2  14982  fsumnn0cl  15659  binom  15753  bcxmas  15758  isumnn0nn  15765  climcndslem1  15772  geoser  15790  geomulcvg  15799  risefac0  15950  fallfac0  15951  risefac1  15956  fallfac1  15957  binomfallfaclem2  15963  binomfallfac  15964  bpoly0  15973  bpoly2  15980  bpoly3  15981  bpoly4  15982  fsumcube  15983  ef0lem  16001  ege2le3  16013  ef4p  16038  efgt1p2  16039  efgt1p  16040  ruclem11  16165  nthruz  16178  nn0o  16310  ndvdssub  16336  5ndvds3  16340  bits0  16355  0bits  16366  sadcf  16380  sadc0  16381  sadcaddlem  16384  sadcadd  16385  sadadd2lem  16386  sadadd2  16387  smupf  16405  smup0  16406  smumullem  16419  gcdcl  16433  nn0seqcvgd  16497  algcvg  16503  eucalg  16514  lcmcl  16528  lcmfval  16548  lcmfcl  16555  pclem  16766  pcfac  16827  vdwap0  16904  vdwap1  16905  vdwlem6  16914  hashbc0  16933  0ram  16948  0ramcl  16951  ramz2  16952  ramz  16953  ramcl  16957  prmo0  16964  dec5dvds2  16993  2exp11  17017  2exp16  17018  11prm  17042  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  plendxnocndx  17304  slotsdifdsndx  17314  slotsdifunifndx  17321  odrngstr  17323  slotsdifplendx2  17336  imasvalstr  17371  ipostr  18452  gsumws1  18763  cycsubm  19131  psgnunilem2  19424  psgnunilem3  19425  odfval  19461  oddvdsnn0  19473  pgp0  19525  sylow1lem1  19527  cyggex2  19826  telgsums  19922  srgbinomlem3  20163  srgbinomlem4  20164  srgbinom  20166  cnfldstr  21311  cnfldstrOLD  21326  nn0subm  21377  expmhm  21391  nn0srg  21392  znf1o  21506  zzngim  21507  cygznlem1  21521  cygznlem2a  21522  cygznlem3  21524  cygth  21526  freshmansdream  21529  snifpsrbag  21876  fczpsrbag  21877  psrbagaddcl  21880  psrlidm  21917  mvrf1  21941  mplcoe3  21993  mplcoe5  21995  ltbwe  21999  psrbag0  22017  psrbagsn  22018  evlslem1  22037  mhpsclcl  22090  mhpmulcl  22092  psdmul  22109  psdmvr  22112  00ply1bas  22180  ply1plusgfvi  22182  coe1sclmul  22224  coe1sclmul2  22226  coe1scl  22229  ply1sclid  22230  ply1idvr1OLD  22239  cply1coe0bi  22246  ply1scleq  22249  cpm2mf  22696  m2cpminvid2lem  22698  m2cpminvid2  22699  m2cpmfo  22700  decpmatid  22714  pmatcollpw3  22728  pmatcollpw3fi1lem1  22730  pmatcollpwscmatlem1  22733  pmatcollpwscmatlem2  22734  idpm2idmp  22745  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  cpmadugsumlemF  22820  dscmet  24516  ehl0base  25372  ehl0  25373  itgcnlem  25747  dvn0  25882  dvn1  25884  cpncn  25894  dveflem  25939  c1lip2  25959  deg1le0  26072  ply1divex  26098  mon1pid  26115  ply1rem  26127  fta1g  26131  plyconst  26167  plypf1  26173  plyco  26202  0dgr  26206  0dgrb  26207  coefv0  26209  dgreq0  26227  vieta1lem2  26275  vieta1  26276  aareccl  26290  aannenlem2  26293  taylthlem1  26337  radcnv0  26381  abelthlem6  26402  abelthlem9  26406  logtayl  26625  cxp0  26635  cxpeq  26723  leibpilem2  26907  leibpi  26908  log2ublem3  26914  log2ub  26915  log2le1  26916  divsqrtsumlem  26946  dmgmn0  26992  lgambdd  27003  sqff1o  27148  ppiublem2  27170  chtublem  27178  bclbnd  27247  bposlem8  27258  lgsval  27268  dchrisum0flblem1  27475  dchrisum0flb  27477  ostth2lem2  27601  usgrexmplef  29332  usgr0edg0rusgr  29649  usgr2pthlem  29836  wwlksn0s  29934  rusgrnumwwlkb0  30047  erclwwlkref  30095  clwwlkf1  30124  0wlkonlem1  30193  upgr4cycl4dv4e  30260  1kp2ke3k  30521  ex-fac  30526  ex-prmo  30534  nn0min  32901  dpmul1000  32980  dp0h  32983  dpexpp1  32989  dpmul4  32995  threehalves  32996  1mhdrd  32997  s1f1  33025  s2f1  33027  cshw1s2  33042  cycpm2tr  33201  deg1le0eq0  33654  ply1unit  33656  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  ply1dg1rt  33661  m1pmeq  33666  psrbasfsupp  33693  mplmulmvr  33704  evlextv  33707  mplvrpmlem  33708  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  esplyfval0  33722  esplylem  33724  esplyfv1  33727  esplyind  33731  vietalem  33735  vieta  33736  minplyirredlem  33867  rtelextdg2lem  33883  fldext2chn  33885  constraddcl  33919  constrnegcl  33920  constrdircl  33922  constrremulcl  33924  2sqr3minply  33937  lmatcl  33973  lmat22e12  33976  lmat22e21  33977  fsumcvg4  34107  oddpwdc  34511  eulerpartlems  34517  eulerpartlemb  34525  eulerpartlemt  34528  eulerpartgbij  34529  eulerpartlemmf  34532  eulerpartlemgf  34536  eulerpartlemgs2  34537  eulerpartlemn  34538  fib0  34556  fib1  34557  fibp1  34558  ofcs1  34701  signsply0  34708  signsvvf  34736  prodfzo03  34760  repr0  34768  breprexp  34790  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  tgoldbachgtde  34817  0nn0m1nnn0  35307  f1resfz0f1d  35308  usgrgt2cycl  35324  subfac0  35371  subfacval2  35381  subfaclim  35382  cvmliftlem7  35485  cvmliftlem13  35490  bccolsum  35933  fwddifn0  36358  heiborlem4  38015  heiborlem10  38021  12gcd5e1  42257  60gcd6e6  42258  60gcd7e1  42259  420gcd8e4  42260  12lcm5e60  42262  60lcm7e420  42264  420lcm8e840  42265  lcmineqlem  42306  3exp7  42307  3lexlogpow5ineq1  42308  3lexlogpow5ineq2  42309  3lexlogpow5ineq5  42314  aks4d1p1  42330  aks6d1c2lem4  42381  aks6d1c2  42384  sticksstones11  42410  sticksstones22  42422  aks6d1c7lem1  42434  sqn5i  42540  decpmul  42543  sqdeccom12  42544  sq3deccom12  42545  235t711  42560  ex-decpmul  42561  mhphflem  42839  0prjspn  42871  sum9cubes  42915  nacsfix  42954  diophrw  43001  pell1qr1  43113  monotoddzzfi  43184  jm2.23  43238  hbtlem5  43370  mncn0  43381  aaitgo  43404  brfvrcld  43932  corclrcl  43948  dfrtrcl3  43974  fvrtrcllb0d  43976  fvrtrcllb0da  43977  corcltrcl  43980  cotrclrcl  43983  k0004val0  44395  bccn0  44584  bccn1  44585  binomcxplemradcnv  44593  binomcxplemnotnn0  44597  rexanuz2nf  45736  dvnmul  46187  dvnprodlem3  46192  wallispilem2  46310  wallispi2lem2  46316  stirlinglem5  46322  stirlinglem7  46324  fourierdlem83  46433  fourierdlem112  46462  fouriersw  46475  elaa2lem  46477  elaa2  46478  etransclem48  46526  etransc  46527  iccelpart  47679  fmtno0  47786  fmtnorec2  47789  fmtno5lem1  47799  fmtno5lem2  47800  fmtno5lem4  47802  257prm  47807  fmtnofac2  47815  fmtnofac1  47816  fmtno4prmfac  47818  fmtno4nprmfac193  47820  fmtno5faclem1  47825  fmtno5faclem2  47826  fmtno5faclem3  47827  fmtno5fac  47828  fmtno5nprm  47829  139prmALT  47842  31prm  47843  127prm  47845  m11nprm  47847  bits0ALTV  47925  2exp340mod341  47979  nfermltl2rev  47989  evengpoap3  48045  tgoldbachlt  48062  tgoldbach  48063  stgr0  48206  usgrexmpl1lem  48267  usgrexmpl2lem  48272  gpgprismgr4cycllem6  48346  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem10  48350  nn0mnd  48425  ssnn0ssfz  48595  dig1  48854  0dig2nn0e  48858  0dig2nn0o  48859  0aryfvalel  48880  itcoval0  48908  itcoval1  48909  ackval0  48926  ackval1  48927  ackvalsuc0val  48933  ackval0012  48935  ackval1012  48936  ackval2012  48937  ackval3012  48938  ackval41a  48940