Theorem 0nn0 12515

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 2769	. 2 ⊢ 0 = 0
2		elnn0 12502	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 231	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 889	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 860   = wceq 1567   ∈ wcel 2149  0cc0 11096  ℕcn 12229  ℕ₀cn0 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-mulcl 11158  ax-i2m1 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4592  df-n0 12501

This theorem is referenced by:  0xnn0  12579  nn0ind-raph  12692  10nn0  12729  declei  12748  numlti  12749  nummul1c  12761  decaddc2  12768  decrmanc  12769  decrmac  12770  decaddm10  12771  decaddi  12772  decaddci  12773  decaddci2  12774  decmul1  12776  decmulnc  12779  6p5e11  12785  7p4e11  12788  8p3e11  12793  9p2e11  12799  10p10e20  12807  xnn0n0n1ge2b  13153  0elfz  13648  4fvwrd4  13672  fvinim0ffz  13814  ssnn0fi  14017  fsuppmapnn0fiubex  14024  exple1  14209  nn0opth2  14304  faclbnd4lem3  14327  bc0k  14343  bcn1  14345  bccl  14354  hasheq0  14395  hashrabrsn  14404  hashbc  14486  fi1uzind  14540  brfi1ind  14542  opfi1ind  14545  iswrdi  14550  wrdnfi  14581  s1fv  14644  ccat2s1fst  14673  splfv2a  14789  repsw0  14810  0csh0  14826  cshw1  14855  s2fv0  14920  s3fv0  14924  s4fv0  14928  pfx2  14980  ofs1  15003  relexp0g  15055  relexpaddg  15086  rtrclreclem2  15092  fsumnn0cl  15783  binom  15880  bcxmas  15885  isumnn0nn  15892  climcndslem1  15899  geoser  15917  geomulcvg  15926  risefac0  16077  fallfac0  16078  risefac1  16083  fallfac1  16084  binomfallfaclem2  16090  binomfallfac  16091  bpoly0  16100  bpoly2  16107  bpoly3  16108  bpoly4  16109  fsumcube  16110  ef0lem  16128  ege2le3  16140  ef4p  16165  efgt1p2  16166  efgt1p  16167  ruclem11  16292  nthruz  16305  nn0o  16437  ndvdssub  16463  5ndvds3  16467  bits0  16482  0bits  16493  sadcf  16507  sadc0  16508  sadcaddlem  16511  sadcadd  16512  sadadd2lem  16513  sadadd2  16514  smupf  16532  smup0  16533  smumullem  16546  gcdcl  16560  nn0seqcvgd  16624  algcvg  16630  eucalg  16641  lcmcl  16655  lcmfval  16675  lcmfcl  16682  pclem  16894  pcfac  16955  vdwap0  17032  vdwap1  17033  vdwlem6  17042  hashbc0  17061  0ram  17076  0ramcl  17079  ramz2  17080  ramz  17081  ramcl  17085  prmo0  17092  dec5dvds2  17121  2exp11  17145  2exp16  17146  10nprm  17169  11prm  17171  37prm  17177  43prm  17178  83prm  17179  139prm  17180  163prm  17181  317prm  17182  631prm  17183  1259lem1  17187  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  2503lem1  17193  2503lem2  17194  2503lem3  17195  2503prm  17196  4001lem1  17197  4001lem2  17198  4001lem3  17199  4001lem4  17200  4001prm  17201  plendxnocndx  17433  slotsdifdsndx  17443  slotsdifunifndx  17450  odrngstr  17452  slotsdifplendx2  17465  imasvalstr  17500  ipostr  18581  gsumws1  18893  cycsubm  19269  psgnunilem2  19561  psgnunilem3  19562  odfval  19598  oddvdsnn0  19610  pgp0  19662  sylow1lem1  19664  cyggex2  19963  telgsums  20059  srgbinomlem3  20306  srgbinomlem4  20307  srgbinom  20309  cnfldstr  21489  nn0subm  21537  expmhm  21551  nn0srg  21552  znf1o  21666  zzngim  21667  cygznlem1  21681  cygznlem2a  21682  cygznlem3  21684  cygth  21686  freshmansdream  21689  snifpsrbag  22035  fczpsrbag  22036  psrbagaddcl  22039  psrlidm  22076  mvrf1  22100  mplcoe3  22154  mplcoe5  22156  ltbwe  22160  psrbag0  22178  psrbagsn  22179  evlslem1  22198  mhpsclcl  22275  mhpmulcl  22277  psdmul  22294  psdmvr  22297  00ply1bas  22364  ply1plusgfvi  22366  coe1sclmul  22408  coe1sclmul2  22410  coe1scl  22413  ply1sclid  22414  cply1coe0bi  22427  ply1scleq  22430  cpm2mf  22874  m2cpminvid2lem  22876  m2cpminvid2  22877  m2cpmfo  22878  decpmatid  22892  pmatcollpw3  22906  pmatcollpw3fi1lem1  22908  pmatcollpwscmatlem1  22911  pmatcollpwscmatlem2  22912  idpm2idmp  22923  chfacfscmulgsum  22982  chfacfpmmulgsum  22986  cpmadugsumlemF  22998  dscmet  24694  ehl0base  25540  ehl0  25541  itgcnlem  25914  dvn0  26048  dvn1  26050  cpncn  26060  dveflem  26103  c1lip2  26122  deg1le0  26233  ply1divex  26259  mon1pid  26276  ply1rem  26288  fta1g  26292  plyconst  26328  plypf1  26334  plyco  26363  0dgr  26367  0dgrb  26368  coefv0  26370  dgreq0  26387  vieta1lem2  26437  vieta1  26438  aareccl  26452  aannenlem2  26455  taylthlem1  26498  radcnv0  26541  abelthlem6  26561  abelthlem9  26565  logtayl  26787  cxp0  26797  cxpeq  26884  leibpilem2  27068  leibpi  27069  log2ublem3  27075  log2ub  27076  log2le1  27077  divsqrtsumlem  27106  dmgmn0  27152  lgambdd  27163  sqff1o  27308  ppiublem2  27329  chtublem  27337  bclbnd  27406  bposlem8  27417  lgsval  27427  dchrisum0flblem1  27634  dchrisum0flb  27636  ostth2lem2  27760  usgrexmplef  29546  usgr0edg0rusgr  29862  usgr2pthlem  30049  wwlksn0s  30147  rusgrnumwwlkb0  30260  erclwwlkref  30308  clwwlkf1  30337  0wlkonlem1  30406  upgr4cycl4dv4e  30473  1kp2ke3k  30734  ex-fac  30739  ex-prmo  30747  nn0min  33102  dpmul1000  33155  dp0h  33158  dpexpp1  33164  dpmul4  33170  threehalves  33171  1mhdrd  33172  s1f1  33200  s2f1  33202  cshw1s2  33217  cycpm2tr  33376  deg1le0eq0  33804  ply1unit  33806  evl1deg1  33807  evl1deg2  33808  evl1deg3  33809  ply1dg1rt  33811  m1pmeq  33816  psrbasfsupp  33842  mplmulmvr  33870  evlextv  33873  mplvrpmlem  33874  mplvrpmfgalem  33875  mplvrpmga  33876  mplvrpmmhm  33877  mplvrpmrhm  33878  psrmonprod  33883  esplyfval0  33895  esplylem  33897  esplyfv1  33900  esplyfval1  33904  esplyfvaln  33905  esplyind  33906  vietalem  33910  vieta  33911  minplyirredlem  34041  rtelextdg2lem  34057  fldext2chn  34059  constraddcl  34093  constrnegcl  34094  constrdircl  34096  constrremulcl  34098  2sqr3minply  34111  lmatcl  34147  lmat22e12  34150  lmat22e21  34151  fsumcvg4  34281  oddpwdc  34685  eulerpartlems  34691  eulerpartlemb  34699  eulerpartlemt  34702  eulerpartgbij  34703  eulerpartlemmf  34706  eulerpartlemgf  34710  eulerpartlemgs2  34711  eulerpartlemn  34712  fib0  34730  fib1  34731  fibp1  34732  ofcs1  34875  signsply0  34879  signsvvf  34907  prodfzo03  34931  repr0  34939  breprexp  34961  hgt750lemd  34976  hgt750lem  34979  hgt750lem2  34980  hgt750leme  34986  tgoldbachgtde  34988  0nn0m1nnn0  35499  f1resfz0f1d  35500  usgrgt2cycl  35517  subfac0  35564  subfacval2  35574  subfaclim  35575  cvmliftlem7  35678  cvmliftlem13  35683  bccolsum  36126  fwddifn0  36551  heiborlem4  38348  heiborlem10  38354  12gcd5e1  42655  60gcd6e6  42656  60gcd7e1  42657  420gcd8e4  42658  12lcm5e60  42660  60lcm7e420  42662  420lcm8e840  42663  lcmineqlem  42704  3exp7  42705  3lexlogpow5ineq1  42706  3lexlogpow5ineq2  42707  3lexlogpow5ineq5  42712  aks4d1p1  42728  aks6d1c2lem4  42779  aks6d1c2  42782  sticksstones11  42808  sticksstones22  42820  aks6d1c7lem1  42832  25or6to4  42858  sqn5i  42931  decpmul  42934  sqdeccom12  42935  sq3deccom12  42936  235t711  42951  ex-decpmul  42952  mhphflem  43215  0prjspn  43247  sum9cubes  43291  nacsfix  43330  diophrw  43377  pell1qr1  43485  monotoddzzfi  43556  jm2.23  43610  hbtlem5  43742  mncn0  43753  aaitgo  43776  brfvrcld  44304  corclrcl  44320  dfrtrcl3  44346  fvrtrcllb0d  44348  fvrtrcllb0da  44349  corcltrcl  44352  cotrclrcl  44355  k0004val0  44767  bccn0  44940  bccn1  44941  binomcxplemradcnv  44949  binomcxplemnotnn0  44953  rexanuz2nf  46093  dvnmul  46544  dvnprodlem3  46549  wallispilem2  46667  wallispi2lem2  46673  stirlinglem5  46679  stirlinglem7  46681  fourierdlem83  46790  fourierdlem112  46819  fouriersw  46832  elaa2lem  46834  elaa2  46835  etransclem48  46883  etransc  46884  iccelpart  48066  fmtno0  48176  fmtnorec2  48179  fmtno5lem1  48189  fmtno5lem2  48190  fmtno5lem4  48192  257prm  48197  fmtnofac2  48205  fmtnofac1  48206  fmtno4prmfac  48208  fmtno4nprmfac193  48210  fmtno5faclem1  48215  fmtno5faclem2  48216  fmtno5faclem3  48217  fmtno5fac  48218  fmtno5nprm  48219  139prmALT  48232  31prm  48233  127prm  48235  m11nprm  48237  bits0ALTV  48328  2exp340mod341  48382  nfermltl2rev  48392  evengpoap3  48448  tgoldbachlt  48465  tgoldbach  48466  stgr0  48609  usgrexmpl1lem  48670  usgrexmpl2lem  48675  gpgprismgr4cycllem6  48749  gpgprismgr4cycllem7  48750  gpgprismgr4cycllem10  48753  nn0mnd  48828  ssnn0ssfz  49009  dig1  49268  0dig2nn0e  49272  0dig2nn0o  49273  0aryfvalel  49294  itcoval0  49322  itcoval1  49323  ackval0  49340  ackval1  49341  ackvalsuc0val  49347  ackval0012  49349  ackval1012  49350  ackval2012  49351  ackval3012  49352  ackval41a  49354