Theorem 0nn0 12443

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 2739	. 2 ⊢ 0 = 0
2		elnn0 12430	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 229	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 882	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 853   = wceq 1547   ∈ wcel 2119  0cc0 11029  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-n0 12429

This theorem is referenced by:  0xnn0  12507  nn0ind-raph  12620  10nn0  12653  declei  12671  numlti  12672  nummul1c  12684  decaddc2  12691  decrmanc  12692  decrmac  12693  decaddm10  12694  decaddi  12695  decaddci  12696  decaddci2  12697  decmul1  12699  decmulnc  12702  6p5e11  12708  7p4e11  12711  8p3e11  12716  9p2e11  12722  10p10e20  12730  xnn0n0n1ge2b  13074  0elfz  13569  4fvwrd4  13593  fvinim0ffz  13735  ssnn0fi  13938  fsuppmapnn0fiubex  13945  exple1  14130  nn0opth2  14225  faclbnd4lem3  14248  bc0k  14264  bcn1  14266  bccl  14275  hasheq0  14316  hashrabrsn  14325  hashbc  14406  fi1uzind  14460  brfi1ind  14462  opfi1ind  14465  iswrdi  14470  wrdnfi  14501  s1fv  14564  ccat2s1fst  14593  splfv2a  14709  repsw0  14730  0csh0  14746  cshw1  14775  s2fv0  14840  s3fv0  14844  s4fv0  14848  pfx2  14900  ofs1  14923  relexp0g  14975  relexpaddg  15006  rtrclreclem2  15012  fsumnn0cl  15689  binom  15786  bcxmas  15791  isumnn0nn  15798  climcndslem1  15805  geoser  15823  geomulcvg  15832  risefac0  15983  fallfac0  15984  risefac1  15989  fallfac1  15990  binomfallfaclem2  15996  binomfallfac  15997  bpoly0  16006  bpoly2  16013  bpoly3  16014  bpoly4  16015  fsumcube  16016  ef0lem  16034  ege2le3  16046  ef4p  16071  efgt1p2  16072  efgt1p  16073  ruclem11  16198  nthruz  16211  nn0o  16343  ndvdssub  16369  5ndvds3  16373  bits0  16388  0bits  16399  sadcf  16413  sadc0  16414  sadcaddlem  16417  sadcadd  16418  sadadd2lem  16419  sadadd2  16420  smupf  16438  smup0  16439  smumullem  16452  gcdcl  16466  nn0seqcvgd  16530  algcvg  16536  eucalg  16547  lcmcl  16561  lcmfval  16581  lcmfcl  16588  pclem  16800  pcfac  16861  vdwap0  16938  vdwap1  16939  vdwlem6  16948  hashbc0  16967  0ram  16982  0ramcl  16985  ramz2  16986  ramz  16987  ramcl  16991  prmo0  16998  dec5dvds2  17027  2exp11  17051  2exp16  17052  11prm  17076  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  plendxnocndx  17338  slotsdifdsndx  17348  slotsdifunifndx  17355  odrngstr  17357  slotsdifplendx2  17370  imasvalstr  17405  ipostr  18486  gsumws1  18797  cycsubm  19168  psgnunilem2  19461  psgnunilem3  19462  odfval  19498  oddvdsnn0  19510  pgp0  19562  sylow1lem1  19564  cyggex2  19863  telgsums  19959  srgbinomlem3  20200  srgbinomlem4  20201  srgbinom  20203  cnfldstr  21349  nn0subm  21397  expmhm  21411  nn0srg  21412  znf1o  21526  zzngim  21527  cygznlem1  21541  cygznlem2a  21542  cygznlem3  21544  cygth  21546  freshmansdream  21549  snifpsrbag  21895  fczpsrbag  21896  psrbagaddcl  21899  psrlidm  21936  mvrf1  21960  mplcoe3  22014  mplcoe5  22016  ltbwe  22020  psrbag0  22038  psrbagsn  22039  evlslem1  22058  mhpsclcl  22135  mhpmulcl  22137  psdmul  22154  psdmvr  22157  00ply1bas  22224  ply1plusgfvi  22226  coe1sclmul  22268  coe1sclmul2  22270  coe1scl  22273  ply1sclid  22274  ply1idvr1OLD  22281  cply1coe0bi  22288  ply1scleq  22291  cpm2mf  22735  m2cpminvid2lem  22737  m2cpminvid2  22738  m2cpmfo  22739  decpmatid  22753  pmatcollpw3  22767  pmatcollpw3fi1lem1  22769  pmatcollpwscmatlem1  22772  pmatcollpwscmatlem2  22773  idpm2idmp  22784  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  cpmadugsumlemF  22859  dscmet  24555  ehl0base  25401  ehl0  25402  itgcnlem  25775  dvn0  25909  dvn1  25911  cpncn  25921  dveflem  25964  c1lip2  25983  deg1le0  26094  ply1divex  26120  mon1pid  26137  ply1rem  26149  fta1g  26153  plyconst  26189  plypf1  26195  plyco  26224  0dgr  26228  0dgrb  26229  coefv0  26231  dgreq0  26248  vieta1lem2  26295  vieta1  26296  aareccl  26310  aannenlem2  26313  taylthlem1  26356  radcnv0  26399  abelthlem6  26419  abelthlem9  26423  logtayl  26642  cxp0  26652  cxpeq  26739  leibpilem2  26923  leibpi  26924  log2ublem3  26930  log2ub  26931  log2le1  26932  divsqrtsumlem  26961  dmgmn0  27007  lgambdd  27018  sqff1o  27163  ppiublem2  27184  chtublem  27192  bclbnd  27261  bposlem8  27272  lgsval  27282  dchrisum0flblem1  27489  dchrisum0flb  27491  ostth2lem2  27615  usgrexmplef  29346  usgr0edg0rusgr  29662  usgr2pthlem  29849  wwlksn0s  29947  rusgrnumwwlkb0  30060  erclwwlkref  30108  clwwlkf1  30137  0wlkonlem1  30206  upgr4cycl4dv4e  30273  1kp2ke3k  30534  ex-fac  30539  ex-prmo  30547  nn0min  32913  dpmul1000  32977  dp0h  32980  dpexpp1  32986  dpmul4  32992  threehalves  32993  1mhdrd  32994  s1f1  33022  s2f1  33024  cshw1s2  33039  cycpm2tr  33200  deg1le0eq0  33656  ply1unit  33658  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  ply1dg1rt  33663  m1pmeq  33668  psrbasfsupp  33695  mplmulmvr  33723  evlextv  33726  mplvrpmlem  33727  mplvrpmfgalem  33728  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  psrmonprod  33736  esplyfval0  33748  esplylem  33750  esplyfv1  33753  esplyfval1  33757  esplyfvaln  33758  esplyind  33759  vietalem  33763  vieta  33764  minplyirredlem  33894  rtelextdg2lem  33910  fldext2chn  33912  constraddcl  33946  constrnegcl  33947  constrdircl  33949  constrremulcl  33951  2sqr3minply  33964  lmatcl  34000  lmat22e12  34003  lmat22e21  34004  fsumcvg4  34134  oddpwdc  34538  eulerpartlems  34544  eulerpartlemb  34552  eulerpartlemt  34555  eulerpartgbij  34556  eulerpartlemmf  34559  eulerpartlemgf  34563  eulerpartlemgs2  34564  eulerpartlemn  34565  fib0  34583  fib1  34584  fibp1  34585  ofcs1  34728  signsply0  34735  signsvvf  34763  prodfzo03  34787  repr0  34795  breprexp  34817  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  tgoldbachgtde  34844  0nn0m1nnn0  35341  f1resfz0f1d  35342  usgrgt2cycl  35358  subfac0  35405  subfacval2  35415  subfaclim  35416  cvmliftlem7  35519  cvmliftlem13  35524  bccolsum  35967  fwddifn0  36392  heiborlem4  38181  heiborlem10  38187  12gcd5e1  42488  60gcd6e6  42489  60gcd7e1  42490  420gcd8e4  42491  12lcm5e60  42493  60lcm7e420  42495  420lcm8e840  42496  lcmineqlem  42537  3exp7  42538  3lexlogpow5ineq1  42539  3lexlogpow5ineq2  42540  3lexlogpow5ineq5  42545  aks4d1p1  42561  aks6d1c2lem4  42612  aks6d1c2  42615  sticksstones11  42641  sticksstones22  42653  aks6d1c7lem1  42665  sqn5i  42762  decpmul  42765  sqdeccom12  42766  sq3deccom12  42767  235t711  42782  ex-decpmul  42783  mhphflem  43046  0prjspn  43078  sum9cubes  43122  nacsfix  43161  diophrw  43208  pell1qr1  43316  monotoddzzfi  43387  jm2.23  43441  hbtlem5  43573  mncn0  43584  aaitgo  43607  brfvrcld  44135  corclrcl  44151  dfrtrcl3  44177  fvrtrcllb0d  44179  fvrtrcllb0da  44180  corcltrcl  44183  cotrclrcl  44186  k0004val0  44598  bccn0  44787  bccn1  44788  binomcxplemradcnv  44796  binomcxplemnotnn0  44800  rexanuz2nf  45935  dvnmul  46386  dvnprodlem3  46391  wallispilem2  46509  wallispi2lem2  46515  stirlinglem5  46521  stirlinglem7  46523  fourierdlem83  46632  fourierdlem112  46661  fouriersw  46674  elaa2lem  46676  elaa2  46677  etransclem48  46725  etransc  46726  iccelpart  47908  fmtno0  48018  fmtnorec2  48021  fmtno5lem1  48031  fmtno5lem2  48032  fmtno5lem4  48034  257prm  48039  fmtnofac2  48047  fmtnofac1  48048  fmtno4prmfac  48050  fmtno4nprmfac193  48052  fmtno5faclem1  48057  fmtno5faclem2  48058  fmtno5faclem3  48059  fmtno5fac  48060  fmtno5nprm  48061  139prmALT  48074  31prm  48075  127prm  48077  m11nprm  48079  bits0ALTV  48170  2exp340mod341  48224  nfermltl2rev  48234  evengpoap3  48290  tgoldbachlt  48307  tgoldbach  48308  stgr0  48451  usgrexmpl1lem  48512  usgrexmpl2lem  48517  gpgprismgr4cycllem6  48591  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem10  48595  nn0mnd  48670  ssnn0ssfz  48840  dig1  49099  0dig2nn0e  49103  0dig2nn0o  49104  0aryfvalel  49125  itcoval0  49153  itcoval1  49154  ackval0  49171  ackval1  49172  ackvalsuc0val  49178  ackval0012  49180  ackval1012  49181  ackval2012  49182  ackval3012  49183  ackval41a  49185