Theorem 0nn0 12391

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 2731	. 2 ⊢ 0 = 0
2		elnn0 12378	. . . 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 2111  0cc0 11001  ℕcn 12120  ℕ₀cn0 12376

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-mulcl 11063  ax-i2m1 11069

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4572  df-n0 12377

This theorem is referenced by:  0xnn0  12455  nn0ind-raph  12568  10nn0  12601  declei  12619  numlti  12620  nummul1c  12632  decaddc2  12639  decrmanc  12640  decrmac  12641  decaddm10  12642  decaddi  12643  decaddci  12644  decaddci2  12645  decmul1  12647  decmulnc  12650  6p5e11  12656  7p4e11  12659  8p3e11  12664  9p2e11  12670  10p10e20  12678  xnn0n0n1ge2b  13026  0elfz  13519  4fvwrd4  13543  fvinim0ffz  13684  ssnn0fi  13887  fsuppmapnn0fiubex  13894  exple1  14079  nn0opth2  14174  faclbnd4lem3  14197  bc0k  14213  bcn1  14215  bccl  14224  hasheq0  14265  hashrabrsn  14274  hashbc  14355  fi1uzind  14409  brfi1ind  14411  opfi1ind  14414  iswrdi  14419  wrdnfi  14450  s1fv  14513  ccat2s1fst  14542  splfv2a  14658  repsw0  14679  0csh0  14695  cshw1  14724  s2fv0  14789  s3fv0  14793  s4fv0  14797  pfx2  14849  ofs1  14872  relexp0g  14924  relexpaddg  14955  rtrclreclem2  14961  fsumnn0cl  15638  binom  15732  bcxmas  15737  isumnn0nn  15744  climcndslem1  15751  geoser  15769  geomulcvg  15778  risefac0  15929  fallfac0  15930  risefac1  15935  fallfac1  15936  binomfallfaclem2  15942  binomfallfac  15943  bpoly0  15952  bpoly2  15959  bpoly3  15960  bpoly4  15961  fsumcube  15962  ef0lem  15980  ege2le3  15992  ef4p  16017  efgt1p2  16018  efgt1p  16019  ruclem11  16144  nthruz  16157  nn0o  16289  ndvdssub  16315  5ndvds3  16319  bits0  16334  0bits  16345  sadcf  16359  sadc0  16360  sadcaddlem  16363  sadcadd  16364  sadadd2lem  16365  sadadd2  16366  smupf  16384  smup0  16385  smumullem  16398  gcdcl  16412  nn0seqcvgd  16476  algcvg  16482  eucalg  16493  lcmcl  16507  lcmfval  16527  lcmfcl  16534  pclem  16745  pcfac  16806  vdwap0  16883  vdwap1  16884  vdwlem6  16893  hashbc0  16912  0ram  16927  0ramcl  16930  ramz2  16931  ramz  16932  ramcl  16936  prmo0  16943  dec5dvds2  16972  2exp11  16996  2exp16  16997  11prm  17021  37prm  17027  43prm  17028  83prm  17029  139prm  17030  163prm  17031  317prm  17032  631prm  17033  1259lem1  17037  1259lem2  17038  1259lem3  17039  1259lem4  17040  1259lem5  17041  2503lem1  17043  2503lem2  17044  2503lem3  17045  2503prm  17046  4001lem1  17047  4001lem2  17048  4001lem3  17049  4001lem4  17050  4001prm  17051  plendxnocndx  17283  slotsdifdsndx  17293  slotsdifunifndx  17300  odrngstr  17302  slotsdifplendx2  17315  imasvalstr  17350  ipostr  18430  gsumws1  18741  cycsubm  19109  psgnunilem2  19402  psgnunilem3  19403  odfval  19439  oddvdsnn0  19451  pgp0  19503  sylow1lem1  19505  cyggex2  19804  telgsums  19900  srgbinomlem3  20141  srgbinomlem4  20142  srgbinom  20144  cnfldstr  21288  cnfldstrOLD  21303  nn0subm  21354  expmhm  21368  nn0srg  21369  znf1o  21483  zzngim  21484  cygznlem1  21498  cygznlem2a  21499  cygznlem3  21501  cygth  21503  freshmansdream  21506  snifpsrbag  21852  fczpsrbag  21853  psrbagaddcl  21856  psrlidm  21894  mvrf1  21918  mplcoe3  21968  mplcoe5  21970  ltbwe  21974  psrbag0  21992  psrbagsn  21993  evlslem1  22012  mhpsclcl  22057  mhpmulcl  22059  psdmul  22076  psdmvr  22079  00ply1bas  22147  ply1plusgfvi  22149  coe1sclmul  22191  coe1sclmul2  22193  coe1scl  22196  ply1sclid  22197  ply1idvr1OLD  22205  cply1coe0bi  22212  ply1scleq  22215  cpm2mf  22662  m2cpminvid2lem  22664  m2cpminvid2  22665  m2cpmfo  22666  decpmatid  22680  pmatcollpw3  22694  pmatcollpw3fi1lem1  22696  pmatcollpwscmatlem1  22699  pmatcollpwscmatlem2  22700  idpm2idmp  22711  chfacfscmulgsum  22770  chfacfpmmulgsum  22774  cpmadugsumlemF  22786  dscmet  24482  ehl0base  25338  ehl0  25339  itgcnlem  25713  dvn0  25848  dvn1  25850  cpncn  25860  dveflem  25905  c1lip2  25925  deg1le0  26038  ply1divex  26064  mon1pid  26081  ply1rem  26093  fta1g  26097  plyconst  26133  plypf1  26139  plyco  26168  0dgr  26172  0dgrb  26173  coefv0  26175  dgreq0  26193  vieta1lem2  26241  vieta1  26242  aareccl  26256  aannenlem2  26259  taylthlem1  26303  radcnv0  26347  abelthlem6  26368  abelthlem9  26372  logtayl  26591  cxp0  26601  cxpeq  26689  leibpilem2  26873  leibpi  26874  log2ublem3  26880  log2ub  26881  log2le1  26882  divsqrtsumlem  26912  dmgmn0  26958  lgambdd  26969  sqff1o  27114  ppiublem2  27136  chtublem  27144  bclbnd  27213  bposlem8  27224  lgsval  27234  dchrisum0flblem1  27441  dchrisum0flb  27443  ostth2lem2  27567  usgrexmplef  29232  usgr0edg0rusgr  29549  usgr2pthlem  29736  wwlksn0s  29834  rusgrnumwwlkb0  29944  erclwwlkref  29992  clwwlkf1  30021  0wlkonlem1  30090  upgr4cycl4dv4e  30157  1kp2ke3k  30418  ex-fac  30423  ex-prmo  30431  nn0min  32795  dpmul1000  32871  dp0h  32874  dpexpp1  32880  dpmul4  32886  threehalves  32887  1mhdrd  32888  s1f1  32916  s2f1  32918  cshw1s2  32933  cycpm2tr  33080  deg1le0eq0  33528  ply1unit  33530  evl1deg1  33531  evl1deg2  33532  evl1deg3  33533  ply1dg1rt  33535  m1pmeq  33539  psrbasfsupp  33564  mplvrpmlem  33565  mplvrpmfgalem  33566  mplvrpmga  33567  mplvrpmmhm  33568  mplvrpmrhm  33569  esplylem  33579  esplyfv1  33582  minplyirredlem  33715  rtelextdg2lem  33731  fldext2chn  33733  constraddcl  33767  constrnegcl  33768  constrdircl  33770  constrremulcl  33772  2sqr3minply  33785  lmatcl  33821  lmat22e12  33824  lmat22e21  33825  fsumcvg4  33955  oddpwdc  34359  eulerpartlems  34365  eulerpartlemb  34373  eulerpartlemt  34376  eulerpartgbij  34377  eulerpartlemmf  34380  eulerpartlemgf  34384  eulerpartlemgs2  34385  eulerpartlemn  34386  fib0  34404  fib1  34405  fibp1  34406  ofcs1  34549  signsply0  34556  signsvvf  34584  prodfzo03  34608  repr0  34616  breprexp  34638  hgt750lemd  34653  hgt750lem  34656  hgt750lem2  34657  hgt750leme  34663  tgoldbachgtde  34665  0nn0m1nnn0  35149  f1resfz0f1d  35150  usgrgt2cycl  35166  subfac0  35213  subfacval2  35223  subfaclim  35224  cvmliftlem7  35327  cvmliftlem13  35332  bccolsum  35775  fwddifn0  36198  heiborlem4  37854  heiborlem10  37860  12gcd5e1  42036  60gcd6e6  42037  60gcd7e1  42038  420gcd8e4  42039  12lcm5e60  42041  60lcm7e420  42043  420lcm8e840  42044  lcmineqlem  42085  3exp7  42086  3lexlogpow5ineq1  42087  3lexlogpow5ineq2  42088  3lexlogpow5ineq5  42093  aks4d1p1  42109  aks6d1c2lem4  42160  aks6d1c2  42163  sticksstones11  42189  sticksstones22  42201  aks6d1c7lem1  42213  sqn5i  42318  decpmul  42321  sqdeccom12  42322  sq3deccom12  42323  235t711  42338  ex-decpmul  42339  mhphflem  42629  0prjspn  42661  sum9cubes  42705  nacsfix  42745  diophrw  42792  pell1qr1  42904  monotoddzzfi  42975  jm2.23  43029  hbtlem5  43161  mncn0  43172  aaitgo  43195  brfvrcld  43724  corclrcl  43740  dfrtrcl3  43766  fvrtrcllb0d  43768  fvrtrcllb0da  43769  corcltrcl  43772  cotrclrcl  43775  k0004val0  44187  bccn0  44376  bccn1  44377  binomcxplemradcnv  44385  binomcxplemnotnn0  44389  rexanuz2nf  45530  dvnmul  45981  dvnprodlem3  45986  wallispilem2  46104  wallispi2lem2  46110  stirlinglem5  46116  stirlinglem7  46118  fourierdlem83  46227  fourierdlem112  46256  fouriersw  46269  elaa2lem  46271  elaa2  46272  etransclem48  46320  etransc  46321  iccelpart  47464  fmtno0  47571  fmtnorec2  47574  fmtno5lem1  47584  fmtno5lem2  47585  fmtno5lem4  47587  257prm  47592  fmtnofac2  47600  fmtnofac1  47601  fmtno4prmfac  47603  fmtno4nprmfac193  47605  fmtno5faclem1  47610  fmtno5faclem2  47611  fmtno5faclem3  47612  fmtno5fac  47613  fmtno5nprm  47614  139prmALT  47627  31prm  47628  127prm  47630  m11nprm  47632  bits0ALTV  47710  2exp340mod341  47764  nfermltl2rev  47774  evengpoap3  47830  tgoldbachlt  47847  tgoldbach  47848  stgr0  47991  usgrexmpl1lem  48052  usgrexmpl2lem  48057  gpgprismgr4cycllem6  48131  gpgprismgr4cycllem7  48132  gpgprismgr4cycllem10  48135  nn0mnd  48210  ssnn0ssfz  48380  dig1  48640  0dig2nn0e  48644  0dig2nn0o  48645  0aryfvalel  48666  itcoval0  48694  itcoval1  48695  ackval0  48712  ackval1  48713  ackvalsuc0val  48719  ackval0012  48721  ackval1012  48722  ackval2012  48723  ackval3012  48724  ackval41a  48726