Theorem 0nn0 12452

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

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114  0cc0 11038  ℕcn 12174  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-n0 12438

This theorem is referenced by:  0xnn0  12516  nn0ind-raph  12629  10nn0  12662  declei  12680  numlti  12681  nummul1c  12693  decaddc2  12700  decrmanc  12701  decrmac  12702  decaddm10  12703  decaddi  12704  decaddci  12705  decaddci2  12706  decmul1  12708  decmulnc  12711  6p5e11  12717  7p4e11  12720  8p3e11  12725  9p2e11  12731  10p10e20  12739  xnn0n0n1ge2b  13083  0elfz  13578  4fvwrd4  13602  fvinim0ffz  13744  ssnn0fi  13947  fsuppmapnn0fiubex  13954  exple1  14139  nn0opth2  14234  faclbnd4lem3  14257  bc0k  14273  bcn1  14275  bccl  14284  hasheq0  14325  hashrabrsn  14334  hashbc  14415  fi1uzind  14469  brfi1ind  14471  opfi1ind  14474  iswrdi  14479  wrdnfi  14510  s1fv  14573  ccat2s1fst  14602  splfv2a  14718  repsw0  14739  0csh0  14755  cshw1  14784  s2fv0  14849  s3fv0  14853  s4fv0  14857  pfx2  14909  ofs1  14932  relexp0g  14984  relexpaddg  15015  rtrclreclem2  15021  fsumnn0cl  15698  binom  15795  bcxmas  15800  isumnn0nn  15807  climcndslem1  15814  geoser  15832  geomulcvg  15841  risefac0  15992  fallfac0  15993  risefac1  15998  fallfac1  15999  binomfallfaclem2  16005  binomfallfac  16006  bpoly0  16015  bpoly2  16022  bpoly3  16023  bpoly4  16024  fsumcube  16025  ef0lem  16043  ege2le3  16055  ef4p  16080  efgt1p2  16081  efgt1p  16082  ruclem11  16207  nthruz  16220  nn0o  16352  ndvdssub  16378  5ndvds3  16382  bits0  16397  0bits  16408  sadcf  16422  sadc0  16423  sadcaddlem  16426  sadcadd  16427  sadadd2lem  16428  sadadd2  16429  smupf  16447  smup0  16448  smumullem  16461  gcdcl  16475  nn0seqcvgd  16539  algcvg  16545  eucalg  16556  lcmcl  16570  lcmfval  16590  lcmfcl  16597  pclem  16809  pcfac  16870  vdwap0  16947  vdwap1  16948  vdwlem6  16957  hashbc0  16976  0ram  16991  0ramcl  16994  ramz2  16995  ramz  16996  ramcl  17000  prmo0  17007  dec5dvds2  17036  2exp11  17060  2exp16  17061  11prm  17085  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  plendxnocndx  17347  slotsdifdsndx  17357  slotsdifunifndx  17364  odrngstr  17366  slotsdifplendx2  17379  imasvalstr  17414  ipostr  18495  gsumws1  18806  cycsubm  19177  psgnunilem2  19470  psgnunilem3  19471  odfval  19507  oddvdsnn0  19519  pgp0  19571  sylow1lem1  19573  cyggex2  19872  telgsums  19968  srgbinomlem3  20209  srgbinomlem4  20210  srgbinom  20212  cnfldstr  21354  nn0subm  21402  expmhm  21416  nn0srg  21417  znf1o  21531  zzngim  21532  cygznlem1  21546  cygznlem2a  21547  cygznlem3  21549  cygth  21551  freshmansdream  21554  snifpsrbag  21900  fczpsrbag  21901  psrbagaddcl  21904  psrlidm  21940  mvrf1  21964  mplcoe3  22016  mplcoe5  22018  ltbwe  22022  psrbag0  22040  psrbagsn  22041  evlslem1  22060  mhpsclcl  22113  mhpmulcl  22115  psdmul  22132  psdmvr  22135  00ply1bas  22203  ply1plusgfvi  22205  coe1sclmul  22247  coe1sclmul2  22249  coe1scl  22252  ply1sclid  22253  ply1idvr1OLD  22260  cply1coe0bi  22267  ply1scleq  22270  cpm2mf  22717  m2cpminvid2lem  22719  m2cpminvid2  22720  m2cpmfo  22721  decpmatid  22735  pmatcollpw3  22749  pmatcollpw3fi1lem1  22751  pmatcollpwscmatlem1  22754  pmatcollpwscmatlem2  22755  idpm2idmp  22766  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  cpmadugsumlemF  22841  dscmet  24537  ehl0base  25383  ehl0  25384  itgcnlem  25757  dvn0  25891  dvn1  25893  cpncn  25903  dveflem  25946  c1lip2  25965  deg1le0  26076  ply1divex  26102  mon1pid  26119  ply1rem  26131  fta1g  26135  plyconst  26171  plypf1  26177  plyco  26206  0dgr  26210  0dgrb  26211  coefv0  26213  dgreq0  26230  vieta1lem2  26277  vieta1  26278  aareccl  26292  aannenlem2  26295  taylthlem1  26338  radcnv0  26381  abelthlem6  26401  abelthlem9  26405  logtayl  26624  cxp0  26634  cxpeq  26721  leibpilem2  26905  leibpi  26906  log2ublem3  26912  log2ub  26913  log2le1  26914  divsqrtsumlem  26943  dmgmn0  26989  lgambdd  27000  sqff1o  27145  ppiublem2  27166  chtublem  27174  bclbnd  27243  bposlem8  27254  lgsval  27264  dchrisum0flblem1  27471  dchrisum0flb  27473  ostth2lem2  27597  usgrexmplef  29328  usgr0edg0rusgr  29644  usgr2pthlem  29831  wwlksn0s  29929  rusgrnumwwlkb0  30042  erclwwlkref  30090  clwwlkf1  30119  0wlkonlem1  30188  upgr4cycl4dv4e  30255  1kp2ke3k  30516  ex-fac  30521  ex-prmo  30529  nn0min  32894  dpmul1000  32958  dp0h  32961  dpexpp1  32967  dpmul4  32973  threehalves  32974  1mhdrd  32975  s1f1  33003  s2f1  33005  cshw1s2  33020  cycpm2tr  33180  deg1le0eq0  33633  ply1unit  33635  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ply1dg1rt  33640  m1pmeq  33645  psrbasfsupp  33672  mplmulmvr  33683  evlextv  33686  mplvrpmlem  33687  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonprod  33696  esplyfval0  33708  esplylem  33710  esplyfv1  33713  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  vietalem  33723  vieta  33724  minplyirredlem  33854  rtelextdg2lem  33870  fldext2chn  33872  constraddcl  33906  constrnegcl  33907  constrdircl  33909  constrremulcl  33911  2sqr3minply  33924  lmatcl  33960  lmat22e12  33963  lmat22e21  33964  fsumcvg4  34094  oddpwdc  34498  eulerpartlems  34504  eulerpartlemb  34512  eulerpartlemt  34515  eulerpartgbij  34516  eulerpartlemmf  34519  eulerpartlemgf  34523  eulerpartlemgs2  34524  eulerpartlemn  34525  fib0  34543  fib1  34544  fibp1  34545  ofcs1  34688  signsply0  34695  signsvvf  34723  prodfzo03  34747  repr0  34755  breprexp  34777  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  tgoldbachgtde  34804  0nn0m1nnn0  35295  f1resfz0f1d  35296  usgrgt2cycl  35312  subfac0  35359  subfacval2  35369  subfaclim  35370  cvmliftlem7  35473  cvmliftlem13  35478  bccolsum  35921  fwddifn0  36346  heiborlem4  38135  heiborlem10  38141  12gcd5e1  42442  60gcd6e6  42443  60gcd7e1  42444  420gcd8e4  42445  12lcm5e60  42447  60lcm7e420  42449  420lcm8e840  42450  lcmineqlem  42491  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  3lexlogpow5ineq5  42499  aks4d1p1  42515  aks6d1c2lem4  42566  aks6d1c2  42569  sticksstones11  42595  sticksstones22  42607  aks6d1c7lem1  42619  sqn5i  42717  decpmul  42720  sqdeccom12  42721  sq3deccom12  42722  235t711  42737  ex-decpmul  42738  mhphflem  43029  0prjspn  43061  sum9cubes  43105  nacsfix  43144  diophrw  43191  pell1qr1  43299  monotoddzzfi  43370  jm2.23  43424  hbtlem5  43556  mncn0  43567  aaitgo  43590  brfvrcld  44118  corclrcl  44134  dfrtrcl3  44160  fvrtrcllb0d  44162  fvrtrcllb0da  44163  corcltrcl  44166  cotrclrcl  44169  k0004val0  44581  bccn0  44770  bccn1  44771  binomcxplemradcnv  44779  binomcxplemnotnn0  44783  rexanuz2nf  45920  dvnmul  46371  dvnprodlem3  46376  wallispilem2  46494  wallispi2lem2  46500  stirlinglem5  46506  stirlinglem7  46508  fourierdlem83  46617  fourierdlem112  46646  fouriersw  46659  elaa2lem  46661  elaa2  46662  etransclem48  46710  etransc  46711  iccelpart  47893  fmtno0  48003  fmtnorec2  48006  fmtno5lem1  48016  fmtno5lem2  48017  fmtno5lem4  48019  257prm  48024  fmtnofac2  48032  fmtnofac1  48033  fmtno4prmfac  48035  fmtno4nprmfac193  48037  fmtno5faclem1  48042  fmtno5faclem2  48043  fmtno5faclem3  48044  fmtno5fac  48045  fmtno5nprm  48046  139prmALT  48059  31prm  48060  127prm  48062  m11nprm  48064  bits0ALTV  48155  2exp340mod341  48209  nfermltl2rev  48219  evengpoap3  48275  tgoldbachlt  48292  tgoldbach  48293  stgr0  48436  usgrexmpl1lem  48497  usgrexmpl2lem  48502  gpgprismgr4cycllem6  48576  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem10  48580  nn0mnd  48655  ssnn0ssfz  48825  dig1  49084  0dig2nn0e  49088  0dig2nn0o  49089  0aryfvalel  49110  itcoval0  49138  itcoval1  49139  ackval0  49156  ackval1  49157  ackvalsuc0val  49163  ackval0012  49165  ackval1012  49166  ackval2012  49167  ackval3012  49168  ackval41a  49170