Theorem 0nn0 11766

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

Syntax hints:   ∨ wo 842   = wceq 1525   ∈ wcel 2083  0cc0 10390  ℕcn 11492  ℕ₀cn0 11751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-mulcl 10452  ax-i2m1 10458

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-un 3870  df-sn 4479  df-n0 11752

This theorem is referenced by:  0xnn0  11827  nn0ind-raph  11936  10nn0  11970  declei  11988  numlti  11989  nummul1c  12001  decaddc2  12008  decrmanc  12009  decrmac  12010  decaddm10  12011  decaddi  12012  decaddci  12013  decaddci2  12014  decmul1  12016  decmulnc  12019  6p5e11  12025  7p4e11  12028  8p3e11  12033  9p2e11  12039  10p10e20  12047  xnn0n0n1ge2b  12380  0elfz  12858  4fvwrd4  12881  fvinim0ffz  13010  ssnn0fi  13207  fsuppmapnn0fiubex  13214  exple1  13394  nn0opth2  13486  faclbnd4lem3  13509  bc0k  13525  bcn1  13527  bccl  13536  hasheq0  13578  hashrabrsn  13585  hashbc  13663  fi1uzind  13705  brfi1ind  13707  opfi1ind  13710  iswrdi  13715  wrdnfi  13749  s1fv  13812  ccat2s1fst  13841  splfv2a  13958  repsw0  13979  0csh0  13995  cshw1  14024  s2fv0  14089  s3fv0  14093  s4fv0  14097  pfx2  14149  ofs1  14168  relexp0g  14219  relexpaddg  14250  rtrclreclem1  14255  fsumnn0cl  14930  binom  15022  bcxmas  15027  isumnn0nn  15034  climcndslem1  15041  geoser  15059  geomulcvg  15069  risefac0  15218  fallfac0  15219  risefac1  15224  fallfac1  15225  binomfallfaclem2  15231  binomfallfac  15232  bpoly0  15241  bpoly2  15248  bpoly3  15249  bpoly4  15250  fsumcube  15251  ef0lem  15269  ege2le3  15280  ef4p  15303  efgt1p2  15304  efgt1p  15305  ruclem11  15430  nthruz  15443  nn0o  15571  ndvdssub  15597  bits0  15614  0bits  15625  sadcf  15639  sadc0  15640  sadcaddlem  15643  sadcadd  15644  sadadd2lem  15645  sadadd2  15646  smupf  15664  smup0  15665  smumullem  15678  gcdcl  15692  nn0seqcvgd  15747  algcvg  15753  eucalg  15764  lcmcl  15778  lcmfval  15798  lcmfcl  15805  pclem  16008  pcfac  16068  vdwap0  16145  vdwap1  16146  vdwlem6  16155  hashbc0  16174  0ram  16189  0ramcl  16192  ramz2  16193  ramz  16194  ramcl  16198  prmo0  16205  dec5dvds2  16234  2exp16  16257  11prm  16281  37prm  16287  43prm  16288  83prm  16289  139prm  16290  163prm  16291  317prm  16292  631prm  16293  1259lem1  16297  1259lem2  16298  1259lem3  16299  1259lem4  16300  1259lem5  16301  2503lem1  16303  2503lem2  16304  2503lem3  16305  2503prm  16306  4001lem1  16307  4001lem2  16308  4001lem3  16309  4001lem4  16310  4001prm  16311  odrngstr  16512  imasvalstr  16558  ipostr  17596  gsumws1  17819  psgnunilem2  18358  psgnunilem3  18359  odfval  18395  oddvdsnn0  18407  pgp0  18455  sylow1lem1  18457  cyggex2  18742  telgsums  18834  srgbinomlem3  18986  srgbinomlem4  18987  srgbinom  18989  snifpsrbag  19838  fczpsrbag  19839  psrlidm  19875  mvrf1  19897  mplcoe3  19938  mplcoe5  19940  ltbwe  19944  psrbag0  19965  psrbagsn  19966  evlslem1  19986  00ply1bas  20095  ply1plusgfvi  20097  coe1sclmul  20137  coe1sclmul2  20139  coe1scl  20142  ply1sclid  20143  ply1idvr1  20148  cply1coe0bi  20155  cnfldstr  20233  cnfldfun  20243  nn0subm  20286  expmhm  20300  nn0srg  20301  znf1o  20384  zzngim  20385  cygznlem1  20399  cygznlem2a  20400  cygznlem3  20402  cygth  20404  thlle  20527  cpm2mf  21048  m2cpminvid2lem  21050  m2cpminvid2  21051  m2cpmfo  21052  decpmatid  21066  pmatcollpw3  21080  pmatcollpw3fi1lem1  21082  pmatcollpwscmatlem1  21085  pmatcollpwscmatlem2  21086  idpm2idmp  21097  chfacfscmulgsum  21156  chfacfpmmulgsum  21160  cpmadugsumlemF  21172  dscmet  22869  ehl0base  23706  ehl0  23707  itgcnlem  24077  dvn0  24208  dvn1  24210  cpncn  24220  dveflem  24263  c1lip2  24282  tdeglem4  24341  deg1le0  24392  ply1divex  24417  ply1rem  24444  fta1g  24448  plyconst  24483  plypf1  24489  plyco  24518  0dgr  24522  0dgrb  24523  coefv0  24525  dgreq0  24542  vieta1lem2  24587  vieta1  24588  aareccl  24602  aannenlem2  24605  taylthlem1  24648  radcnv0  24691  abelthlem6  24711  abelthlem9  24715  logtayl  24928  cxp0  24938  cxpeq  25023  leibpilem2  25205  leibpi  25206  log2ublem3  25212  log2ub  25213  log2le1  25214  divsqrtsumlem  25243  dmgmn0  25289  lgambdd  25300  sqff1o  25445  ppiublem2  25465  chtublem  25473  bclbnd  25542  bposlem8  25553  lgsval  25563  dchrisum0flblem1  25770  dchrisum0flb  25772  ostth2lem2  25896  usgrexmplef  26728  usgr0edg0rusgr  27044  usgr2pthlem  27230  wwlksn0s  27325  rusgrnumwwlkb0  27436  erclwwlkref  27484  clwwlkf1  27514  0wlkonlem1  27583  upgr4cycl4dv4e  27650  1kp2ke3k  27913  ex-fac  27918  ex-prmo  27926  nn0min  30217  dpmul1000  30255  dp0h  30258  dpexpp1  30264  dpmul4  30270  threehalves  30271  1mhdrd  30272  s2f1  30297  cshw1s2  30304  cycpm2tr  30404  freshmansdream  30509  lmatcl  30692  lmat22e12  30695  lmat22e21  30696  fsumcvg4  30806  oddpwdc  31225  eulerpartlems  31231  eulerpartlemb  31239  eulerpartlemt  31242  eulerpartgbij  31243  eulerpartlemmf  31246  eulerpartlemgf  31250  eulerpartlemgs2  31251  eulerpartlemn  31252  fib0  31270  fib1  31271  fibp1  31272  ofcs1  31427  signsply0  31434  signsvvf  31462  prodfzo03  31487  repr0  31495  breprexp  31517  hgt750lemd  31532  hgt750lem  31535  hgt750lem2  31536  hgt750leme  31542  tgoldbachgtde  31544  0nn0m1nnn0  31961  f1resfz0f1d  31971  usgrgt2cycl  31987  subfac0  32034  subfacval2  32044  subfaclim  32045  cvmliftlem7  32148  cvmliftlem13  32153  bccolsum  32581  fwddifn0  33236  heiborlem4  34645  heiborlem10  34651  sqn5i  38714  decpmul  38717  sqdeccom12  38718  sq3deccom12  38719  235t711  38720  ex-decpmul  38721  0prjspn  38788  nacsfix  38815  diophrw  38862  pell1qr1  38974  monotoddzzfi  39045  jm2.23  39099  hbtlem5  39234  mncn0  39245  aaitgo  39268  mon1pid  39311  brfvrcld  39542  corclrcl  39558  dfrtrcl3  39584  fvrtrcllb0d  39586  fvrtrcllb0da  39587  corcltrcl  39590  cotrclrcl  39593  k0004val0  40010  bccn0  40234  bccn1  40235  binomcxplemradcnv  40243  binomcxplemnotnn0  40247  dvnmul  41791  dvnprodlem3  41796  wallispilem2  41915  wallispi2lem2  41921  stirlinglem5  41927  stirlinglem7  41929  fourierdlem83  42038  fourierdlem112  42067  fouriersw  42080  elaa2lem  42082  elaa2  42083  etransclem48  42131  etransc  42132  iccelpart  43097  fmtno0  43206  fmtnorec2  43209  fmtno5lem1  43219  fmtno5lem2  43220  fmtno5lem4  43222  257prm  43227  fmtnofac2  43235  fmtnofac1  43236  fmtno4prmfac  43238  fmtno4nprmfac193  43240  fmtno5faclem1  43245  fmtno5faclem2  43246  fmtno5faclem3  43247  fmtno5fac  43248  fmtno5nprm  43249  139prmALT  43263  31prm  43264  127prm  43267  2exp11  43269  m11nprm  43270  bits0ALTV  43348  2exp340mod341  43402  nfermltl2rev  43412  evengpoap3  43468  tgoldbachlt  43485  tgoldbach  43486  ssnn0ssfz  43897  dig1  44171  0dig2nn0e  44175  0dig2nn0o  44176