Theorem 0nn0 12484

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 2733	. 2 ⊢ 0 = 0
2		elnn0 12471	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 227	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 875	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 846   = wceq 1542   ∈ wcel 2107  0cc0 11107  ℕcn 12209  ℕ₀cn0 12469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-i2m1 11175

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-sn 4629  df-n0 12470

This theorem is referenced by:  0xnn0  12547  nn0ind-raph  12659  10nn0  12692  declei  12710  numlti  12711  nummul1c  12723  decaddc2  12730  decrmanc  12731  decrmac  12732  decaddm10  12733  decaddi  12734  decaddci  12735  decaddci2  12736  decmul1  12738  decmulnc  12741  6p5e11  12747  7p4e11  12750  8p3e11  12755  9p2e11  12761  10p10e20  12769  xnn0n0n1ge2b  13108  0elfz  13595  4fvwrd4  13618  fvinim0ffz  13748  ssnn0fi  13947  fsuppmapnn0fiubex  13954  exple1  14138  nn0opth2  14229  faclbnd4lem3  14252  bc0k  14268  bcn1  14270  bccl  14279  hasheq0  14320  hashrabrsn  14329  hashbc  14409  fi1uzind  14455  brfi1ind  14457  opfi1ind  14460  iswrdi  14465  wrdnfi  14495  s1fv  14557  ccat2s1fst  14586  splfv2a  14703  repsw0  14724  0csh0  14740  cshw1  14769  s2fv0  14835  s3fv0  14839  s4fv0  14843  pfx2  14895  ofs1  14914  relexp0g  14966  relexpaddg  14997  rtrclreclem2  15003  fsumnn0cl  15679  binom  15773  bcxmas  15778  isumnn0nn  15785  climcndslem1  15792  geoser  15810  geomulcvg  15819  risefac0  15968  fallfac0  15969  risefac1  15974  fallfac1  15975  binomfallfaclem2  15981  binomfallfac  15982  bpoly0  15991  bpoly2  15998  bpoly3  15999  bpoly4  16000  fsumcube  16001  ef0lem  16019  ege2le3  16030  ef4p  16053  efgt1p2  16054  efgt1p  16055  ruclem11  16180  nthruz  16193  nn0o  16323  ndvdssub  16349  bits0  16366  0bits  16377  sadcf  16391  sadc0  16392  sadcaddlem  16395  sadcadd  16396  sadadd2lem  16397  sadadd2  16398  smupf  16416  smup0  16417  smumullem  16430  gcdcl  16444  nn0seqcvgd  16504  algcvg  16510  eucalg  16521  lcmcl  16535  lcmfval  16555  lcmfcl  16562  pclem  16768  pcfac  16829  vdwap0  16906  vdwap1  16907  vdwlem6  16916  hashbc0  16935  0ram  16950  0ramcl  16953  ramz2  16954  ramz  16955  ramcl  16959  prmo0  16966  dec5dvds2  16995  2exp11  17020  2exp16  17021  11prm  17045  37prm  17051  43prm  17052  83prm  17053  139prm  17054  163prm  17055  317prm  17056  631prm  17057  1259lem1  17061  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  2503lem1  17067  2503lem2  17068  2503lem3  17069  2503prm  17070  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  4001prm  17075  plendxnocndx  17326  slotsdifdsndx  17336  slotsdifunifndx  17343  odrngstr  17345  slotsdifplendx2  17359  imasvalstr  17394  ipostr  18479  gsumws1  18716  cycsubm  19074  psgnunilem2  19358  psgnunilem3  19359  odfval  19395  oddvdsnn0  19407  pgp0  19459  sylow1lem1  19461  cyggex2  19760  telgsums  19856  srgbinomlem3  20045  srgbinomlem4  20046  srgbinom  20048  cnfldstr  20939  cnfldfunALTOLD  20951  nn0subm  20993  expmhm  21007  nn0srg  21008  znf1o  21099  zzngim  21100  cygznlem1  21114  cygznlem2a  21115  cygznlem3  21117  cygth  21119  thlleOLD  21244  snifpsrbag  21467  fczpsrbag  21468  psrbagaddcl  21473  psrlidm  21515  mvrf1  21537  mplcoe3  21585  mplcoe5  21587  ltbwe  21591  psrbag0  21615  psrbagsn  21616  evlslem1  21637  mhpsclcl  21682  mhpmulcl  21684  00ply1bas  21754  ply1plusgfvi  21756  coe1sclmul  21796  coe1sclmul2  21798  coe1scl  21801  ply1sclid  21802  ply1idvr1  21809  cply1coe0bi  21816  cpm2mf  22246  m2cpminvid2lem  22248  m2cpminvid2  22249  m2cpmfo  22250  decpmatid  22264  pmatcollpw3  22278  pmatcollpw3fi1lem1  22280  pmatcollpwscmatlem1  22283  pmatcollpwscmatlem2  22284  idpm2idmp  22295  chfacfscmulgsum  22354  chfacfpmmulgsum  22358  cpmadugsumlemF  22370  dscmet  24073  ehl0base  24925  ehl0  24926  itgcnlem  25299  dvn0  25433  dvn1  25435  cpncn  25445  dveflem  25488  c1lip2  25507  tdeglem4OLD  25570  deg1le0  25621  ply1divex  25646  ply1rem  25673  fta1g  25677  plyconst  25712  plypf1  25718  plyco  25747  0dgr  25751  0dgrb  25752  coefv0  25754  dgreq0  25771  vieta1lem2  25816  vieta1  25817  aareccl  25831  aannenlem2  25834  taylthlem1  25877  radcnv0  25920  abelthlem6  25940  abelthlem9  25944  logtayl  26160  cxp0  26170  cxpeq  26255  leibpilem2  26436  leibpi  26437  log2ublem3  26443  log2ub  26444  log2le1  26445  divsqrtsumlem  26474  dmgmn0  26520  lgambdd  26531  sqff1o  26676  ppiublem2  26696  chtublem  26704  bclbnd  26773  bposlem8  26784  lgsval  26794  dchrisum0flblem1  27001  dchrisum0flb  27003  ostth2lem2  27127  usgrexmplef  28506  usgr0edg0rusgr  28822  usgr2pthlem  29010  wwlksn0s  29105  rusgrnumwwlkb0  29215  erclwwlkref  29263  clwwlkf1  29292  0wlkonlem1  29361  upgr4cycl4dv4e  29428  1kp2ke3k  29689  ex-fac  29694  ex-prmo  29702  nn0min  32014  dpmul1000  32053  dp0h  32056  dpexpp1  32062  dpmul4  32068  threehalves  32069  1mhdrd  32070  s1f1  32097  s2f1  32099  cshw1s2  32112  cycpm2tr  32266  freshmansdream  32370  ply1scleq  32628  deg1le0eq0  32644  minplyirredlem  32758  lmatcl  32785  lmat22e12  32788  lmat22e21  32789  fsumcvg4  32919  oddpwdc  33342  eulerpartlems  33348  eulerpartlemb  33356  eulerpartlemt  33359  eulerpartgbij  33360  eulerpartlemmf  33363  eulerpartlemgf  33367  eulerpartlemgs2  33368  eulerpartlemn  33369  fib0  33387  fib1  33388  fibp1  33389  ofcs1  33544  signsply0  33551  signsvvf  33579  prodfzo03  33604  repr0  33612  breprexp  33634  hgt750lemd  33649  hgt750lem  33652  hgt750lem2  33653  hgt750leme  33659  tgoldbachgtde  33661  0nn0m1nnn0  34091  f1resfz0f1d  34092  usgrgt2cycl  34110  subfac0  34157  subfacval2  34167  subfaclim  34168  cvmliftlem7  34271  cvmliftlem13  34276  bccolsum  34698  fwddifn0  35125  heiborlem4  36671  heiborlem10  36677  12gcd5e1  40857  60gcd6e6  40858  60gcd7e1  40859  420gcd8e4  40860  12lcm5e60  40862  60lcm7e420  40864  420lcm8e840  40865  lcmineqlem  40906  3exp7  40907  3lexlogpow5ineq1  40908  3lexlogpow5ineq2  40909  3lexlogpow5ineq5  40914  aks4d1p1  40930  sticksstones11  40961  sticksstones22  40973  mhphflem  41166  sqn5i  41195  decpmul  41198  sqdeccom12  41199  sq3deccom12  41200  235t711  41201  ex-decpmul  41202  0prjspn  41367  nacsfix  41436  diophrw  41483  pell1qr1  41595  monotoddzzfi  41667  jm2.23  41721  hbtlem5  41856  mncn0  41867  aaitgo  41890  mon1pid  41933  brfvrcld  42428  corclrcl  42444  dfrtrcl3  42470  fvrtrcllb0d  42472  fvrtrcllb0da  42473  corcltrcl  42476  cotrclrcl  42479  k0004val0  42891  bccn0  43088  bccn1  43089  binomcxplemradcnv  43097  binomcxplemnotnn0  43101  rexanuz2nf  44190  dvnmul  44646  dvnprodlem3  44651  wallispilem2  44769  wallispi2lem2  44775  stirlinglem5  44781  stirlinglem7  44783  fourierdlem83  44892  fourierdlem112  44921  fouriersw  44934  elaa2lem  44936  elaa2  44937  etransclem48  44985  etransc  44986  iccelpart  46088  fmtno0  46195  fmtnorec2  46198  fmtno5lem1  46208  fmtno5lem2  46209  fmtno5lem4  46211  257prm  46216  fmtnofac2  46224  fmtnofac1  46225  fmtno4prmfac  46227  fmtno4nprmfac193  46229  fmtno5faclem1  46234  fmtno5faclem2  46235  fmtno5faclem3  46236  fmtno5fac  46237  fmtno5nprm  46238  139prmALT  46251  31prm  46252  127prm  46254  m11nprm  46256  bits0ALTV  46334  2exp340mod341  46388  nfermltl2rev  46398  evengpoap3  46454  tgoldbachlt  46471  tgoldbach  46472  nn0mnd  46576  ssnn0ssfz  46979  dig1  47248  0dig2nn0e  47252  0dig2nn0o  47253  0aryfvalel  47274  itcoval0  47302  itcoval1  47303  ackval0  47320  ackval1  47321  ackvalsuc0val  47327  ackval0012  47329  ackval1012  47330  ackval2012  47331  ackval3012  47332  ackval41a  47334  prstclevalOLD  47643