Theorem 0nn0 12514

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 2763	. 2 ⊢ 0 = 0
2		elnn0 12501	. . . 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 1570   ∈ wcel 2143  0cc0 11095  ℕcn 12228  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-i2m1 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-n0 12500

This theorem is referenced by:  0xnn0  12578  nn0ind-raph  12691  10nn0  12728  declei  12747  numlti  12748  nummul1c  12760  decaddc2  12767  decrmanc  12768  decrmac  12769  decaddm10  12770  decaddi  12771  decaddci  12772  decaddci2  12773  decmul1  12775  decmulnc  12778  6p5e11  12784  7p4e11  12787  8p3e11  12792  9p2e11  12798  10p10e20  12806  xnn0n0n1ge2b  13152  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  16076  fallfac0  16077  risefac1  16082  fallfac1  16083  binomfallfaclem2  16089  binomfallfac  16090  bpoly0  16099  bpoly2  16106  bpoly3  16107  bpoly4  16108  fsumcube  16109  ef0lem  16127  ege2le3  16139  ef4p  16164  efgt1p2  16165  efgt1p  16166  ruclem11  16291  nthruz  16304  nn0o  16436  ndvdssub  16462  5ndvds3  16466  bits0  16481  0bits  16492  sadcf  16506  sadc0  16507  sadcaddlem  16510  sadcadd  16511  sadadd2lem  16512  sadadd2  16513  smupf  16531  smup0  16532  smumullem  16545  gcdcl  16559  nn0seqcvgd  16623  algcvg  16629  eucalg  16640  lcmcl  16654  lcmfval  16674  lcmfcl  16681  pclem  16893  pcfac  16954  vdwap0  17031  vdwap1  17032  vdwlem6  17041  hashbc0  17060  0ram  17075  0ramcl  17078  ramz2  17079  ramz  17080  ramcl  17084  prmo0  17091  dec5dvds2  17120  2exp11  17144  2exp16  17145  10nprm  17168  11prm  17170  37prm  17176  43prm  17177  83prm  17178  139prm  17179  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  4001prm  17200  plendxnocndx  17432  slotsdifdsndx  17442  slotsdifunifndx  17449  odrngstr  17451  slotsdifplendx2  17464  imasvalstr  17499  ipostr  18580  gsumws1  18892  cycsubm  19268  psgnunilem2  19560  psgnunilem3  19561  odfval  19597  oddvdsnn0  19609  pgp0  19661  sylow1lem1  19663  cyggex2  19962  telgsums  20058  srgbinomlem3  20305  srgbinomlem4  20306  srgbinom  20308  cnfldstr  21524  nn0subm  21572  expmhm  21586  nn0srg  21587  znf1o  21701  zzngim  21702  cygznlem1  21716  cygznlem2a  21717  cygznlem3  21719  cygth  21721  freshmansdream  21724  snifpsrbag  22070  fczpsrbag  22071  psrbagaddcl  22074  psrlidm  22111  mvrf1  22135  mplcoe3  22189  mplcoe5  22191  ltbwe  22195  psrbag0  22213  psrbagsn  22214  evlslem1  22233  mhpsclcl  22310  mhpmulcl  22312  psdmul  22329  psdmvr  22332  00ply1bas  22399  ply1plusgfvi  22401  coe1sclmul  22443  coe1sclmul2  22445  coe1scl  22448  ply1sclid  22449  cply1coe0bi  22462  ply1scleq  22465  cpm2mf  22909  m2cpminvid2lem  22911  m2cpminvid2  22912  m2cpmfo  22913  decpmatid  22927  pmatcollpw3  22941  pmatcollpw3fi1lem1  22943  pmatcollpwscmatlem1  22946  pmatcollpwscmatlem2  22947  idpm2idmp  22958  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  cpmadugsumlemF  23033  dscmet  24729  ehl0base  25575  ehl0  25576  itgcnlem  25949  dvn0  26083  dvn1  26085  cpncn  26095  dveflem  26138  c1lip2  26157  deg1le0  26268  ply1divex  26294  mon1pid  26311  ply1rem  26323  fta1g  26327  plyconst  26363  plypf1  26369  plyco  26398  0dgr  26402  0dgrb  26403  coefv0  26405  dgreq0  26422  vieta1lem2  26472  vieta1  26473  aareccl  26489  aannenlem2  26492  taylthlem1  26536  radcnv0  26579  abelthlem6  26599  abelthlem9  26603  logtayl  26825  cxp0  26835  cxpeq  26922  leibpilem2  27106  leibpi  27107  log2ublem3  27113  log2ub  27114  log2le1  27115  divsqrtsumlem  27144  dmgmn0  27190  lgambdd  27201  sqff1o  27346  ppiublem2  27367  chtublem  27375  bclbnd  27444  bposlem8  27455  lgsval  27465  dchrisum0flblem1  27672  dchrisum0flb  27674  ostth2lem2  27798  usgrexmplef  29609  usgr0edg0rusgr  29925  usgr2pthlem  30112  wwlksn0s  30210  rusgrnumwwlkb0  30323  erclwwlkref  30371  clwwlkf1  30400  0wlkonlem1  30469  upgr4cycl4dv4e  30536  1kp2ke3k  30797  ex-fac  30802  ex-prmo  30810  nn0min  33165  dpmul1000  33218  dp0h  33221  dpexpp1  33227  dpmul4  33233  threehalves  33234  1mhdrd  33235  s1f1  33263  s2f1  33265  cshw1s2  33280  cycpm2tr  33439  deg1le0eq0  33863  ply1unit  33865  evl1deg1  33866  evl1deg2  33867  evl1deg3  33868  ply1dg1rt  33870  m1pmeq  33875  psrbasfsupp  33901  mplmulmvr  33929  evlextv  33932  mplvrpmlem  33933  mplvrpmfgalem  33934  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  psrmonprod  33942  esplyfval0  33954  esplylem  33956  esplyfv1  33959  esplyfval1  33963  esplyfvaln  33964  esplyind  33965  vietalem  33969  vieta  33970  minplyirredlem  34100  rtelextdg2lem  34116  fldext2chn  34118  constraddcl  34152  constrnegcl  34153  constrdircl  34155  constrremulcl  34157  2sqr3minply  34170  lmatcl  34206  lmat22e12  34209  lmat22e21  34210  fsumcvg4  34340  oddpwdc  34744  eulerpartlems  34750  eulerpartlemb  34758  eulerpartlemt  34761  eulerpartgbij  34762  eulerpartlemmf  34765  eulerpartlemgf  34769  eulerpartlemgs2  34770  eulerpartlemn  34771  fib0  34789  fib1  34790  fibp1  34791  ofcs1  34934  signsply0  34938  signsvvf  34966  prodfzo03  34990  repr0  34998  breprexp  35020  hgt750lemd  35035  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  tgoldbachgtde  35047  0nn0m1nnn0  35604  f1resfz0f1d  35605  usgrgt2cycl  35622  subfac0  35669  subfacval2  35679  subfaclim  35680  cvmliftlem7  35783  cvmliftlem13  35788  bccolsum  36231  fwddifn0  36656  heiborlem4  38465  heiborlem10  38471  12gcd5e1  42770  60gcd6e6  42771  60gcd7e1  42772  420gcd8e4  42773  12lcm5e60  42775  60lcm7e420  42777  420lcm8e840  42778  lcmineqlem  42819  3exp7  42820  3lexlogpow5ineq1  42821  3lexlogpow5ineq2  42822  3lexlogpow5ineq5  42827  aks4d1p1  42843  aks6d1c2lem4  42894  aks6d1c2  42897  sticksstones11  42923  sticksstones22  42935  aks6d1c7lem1  42947  25or6to4  42973  sqn5i  43046  decpmul  43049  sqdeccom12  43050  sq3deccom12  43051  235t711  43066  ex-decpmul  43067  mhphflem  43328  0prjspn  43360  sum9cubes  43404  nacsfix  43443  diophrw  43490  pell1qr1  43598  monotoddzzfi  43669  jm2.23  43723  hbtlem5  43855  mncn0  43866  aaitgo  43889  brfvrcld  44417  corclrcl  44433  dfrtrcl3  44459  fvrtrcllb0d  44461  fvrtrcllb0da  44462  corcltrcl  44465  cotrclrcl  44468  k0004val0  44880  bccn0  45053  bccn1  45054  binomcxplemradcnv  45062  binomcxplemnotnn0  45066  rexanuz2nf  46206  dvnmul  46657  dvnprodlem3  46662  wallispilem2  46780  wallispi2lem2  46786  stirlinglem5  46792  stirlinglem7  46794  fourierdlem83  46903  fourierdlem112  46932  fouriersw  46945  elaa2lem  46947  elaa2  46948  etransclem48  46996  etransc  46997  iccelpart  48182  fmtno0  48292  fmtnorec2  48295  fmtno5lem1  48305  fmtno5lem2  48306  fmtno5lem4  48308  257prm  48313  fmtnofac2  48321  fmtnofac1  48322  fmtno4prmfac  48324  fmtno4nprmfac193  48326  fmtno5faclem1  48331  fmtno5faclem2  48332  fmtno5faclem3  48333  fmtno5fac  48334  fmtno5nprm  48335  139prmALT  48348  31prm  48349  127prm  48351  m11nprm  48353  bits0ALTV  48444  2exp340mod341  48498  nfermltl2rev  48508  evengpoap3  48564  tgoldbachlt  48581  tgoldbach  48582  stgr0  48725  usgrexmpl1lem  48786  usgrexmpl2lem  48791  gpgprismgr4cycllem6  48865  gpgprismgr4cycllem7  48866  gpgprismgr4cycllem10  48869  nn0mnd  48944  ssnn0ssfz  49129  dig1  49388  0dig2nn0e  49392  0dig2nn0o  49393  0aryfvalel  49414  itcoval0  49442  itcoval1  49443  ackval0  49460  ackval1  49461  ackvalsuc0val  49467  ackval0012  49469  ackval1012  49470  ackval2012  49471  ackval3012  49472  ackval41a  49474