Theorem 0nn0 11915

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 2823	. 2 ⊢ 0 = 0
2		elnn0 11902	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 230	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 872	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 843   = wceq 1537   ∈ wcel 2114  0cc0 10539  ℕcn 11640  ℕ₀cn0 11900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-i2m1 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-sn 4570  df-n0 11901

This theorem is referenced by:  0xnn0  11976  nn0ind-raph  12085  10nn0  12119  declei  12137  numlti  12138  nummul1c  12150  decaddc2  12157  decrmanc  12158  decrmac  12159  decaddm10  12160  decaddi  12161  decaddci  12162  decaddci2  12163  decmul1  12165  decmulnc  12168  6p5e11  12174  7p4e11  12177  8p3e11  12182  9p2e11  12188  10p10e20  12196  xnn0n0n1ge2b  12529  0elfz  13007  4fvwrd4  13030  fvinim0ffz  13159  ssnn0fi  13356  fsuppmapnn0fiubex  13363  exple1  13543  nn0opth2  13635  faclbnd4lem3  13658  bc0k  13674  bcn1  13676  bccl  13685  hasheq0  13727  hashrabrsn  13736  hashbc  13814  fi1uzind  13858  brfi1ind  13860  opfi1ind  13863  iswrdi  13868  wrdnfi  13901  s1fv  13966  ccat2s1fst  14002  ccat2s1fstOLD  14003  splfv2a  14120  repsw0  14141  0csh0  14157  cshw1  14186  s2fv0  14251  s3fv0  14255  s4fv0  14259  pfx2  14311  ofs1  14332  relexp0g  14383  relexpaddg  14414  rtrclreclem1  14419  fsumnn0cl  15095  binom  15187  bcxmas  15192  isumnn0nn  15199  climcndslem1  15206  geoser  15224  geomulcvg  15234  risefac0  15383  fallfac0  15384  risefac1  15389  fallfac1  15390  binomfallfaclem2  15396  binomfallfac  15397  bpoly0  15406  bpoly2  15413  bpoly3  15414  bpoly4  15415  fsumcube  15416  ef0lem  15434  ege2le3  15445  ef4p  15468  efgt1p2  15469  efgt1p  15470  ruclem11  15595  nthruz  15608  nn0o  15736  ndvdssub  15762  bits0  15779  0bits  15790  sadcf  15804  sadc0  15805  sadcaddlem  15808  sadcadd  15809  sadadd2lem  15810  sadadd2  15811  smupf  15829  smup0  15830  smumullem  15843  gcdcl  15857  nn0seqcvgd  15916  algcvg  15922  eucalg  15933  lcmcl  15947  lcmfval  15967  lcmfcl  15974  pclem  16177  pcfac  16237  vdwap0  16314  vdwap1  16315  vdwlem6  16324  hashbc0  16343  0ram  16358  0ramcl  16361  ramz2  16362  ramz  16363  ramcl  16367  prmo0  16374  dec5dvds2  16403  2exp16  16426  11prm  16450  37prm  16456  43prm  16457  83prm  16458  139prm  16459  163prm  16460  317prm  16461  631prm  16462  1259lem1  16466  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  2503lem1  16472  2503lem2  16473  2503lem3  16474  2503prm  16475  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001lem4  16479  4001prm  16480  odrngstr  16681  imasvalstr  16727  ipostr  17765  gsumws1  18004  cycsubm  18347  psgnunilem2  18625  psgnunilem3  18626  odfval  18662  oddvdsnn0  18674  pgp0  18723  sylow1lem1  18725  cyggex2  19019  telgsums  19115  srgbinomlem3  19294  srgbinomlem4  19295  srgbinom  19297  snifpsrbag  20148  fczpsrbag  20149  psrlidm  20185  mvrf1  20207  mplcoe3  20249  mplcoe5  20251  ltbwe  20255  psrbag0  20276  psrbagsn  20277  evlslem1  20297  00ply1bas  20410  ply1plusgfvi  20412  coe1sclmul  20452  coe1sclmul2  20454  coe1scl  20457  ply1sclid  20458  ply1idvr1  20463  cply1coe0bi  20470  cnfldstr  20549  cnfldfun  20559  nn0subm  20602  expmhm  20616  nn0srg  20617  znf1o  20700  zzngim  20701  cygznlem1  20715  cygznlem2a  20716  cygznlem3  20718  cygth  20720  thlle  20843  cpm2mf  21362  m2cpminvid2lem  21364  m2cpminvid2  21365  m2cpmfo  21366  decpmatid  21380  pmatcollpw3  21394  pmatcollpw3fi1lem1  21396  pmatcollpwscmatlem1  21399  pmatcollpwscmatlem2  21400  idpm2idmp  21411  chfacfscmulgsum  21470  chfacfpmmulgsum  21474  cpmadugsumlemF  21486  dscmet  23184  ehl0base  24021  ehl0  24022  itgcnlem  24392  dvn0  24523  dvn1  24525  cpncn  24535  dveflem  24578  c1lip2  24597  tdeglem4  24656  deg1le0  24707  ply1divex  24732  ply1rem  24759  fta1g  24763  plyconst  24798  plypf1  24804  plyco  24833  0dgr  24837  0dgrb  24838  coefv0  24840  dgreq0  24857  vieta1lem2  24902  vieta1  24903  aareccl  24917  aannenlem2  24920  taylthlem1  24963  radcnv0  25006  abelthlem6  25026  abelthlem9  25030  logtayl  25245  cxp0  25255  cxpeq  25340  leibpilem2  25521  leibpi  25522  log2ublem3  25528  log2ub  25529  log2le1  25530  divsqrtsumlem  25559  dmgmn0  25605  lgambdd  25616  sqff1o  25761  ppiublem2  25781  chtublem  25789  bclbnd  25858  bposlem8  25869  lgsval  25879  dchrisum0flblem1  26086  dchrisum0flb  26088  ostth2lem2  26212  usgrexmplef  27043  usgr0edg0rusgr  27359  usgr2pthlem  27546  wwlksn0s  27641  rusgrnumwwlkb0  27752  erclwwlkref  27800  clwwlkf1  27830  0wlkonlem1  27899  upgr4cycl4dv4e  27966  1kp2ke3k  28227  ex-fac  28232  ex-prmo  28240  nn0min  30538  dpmul1000  30577  dp0h  30580  dpexpp1  30586  dpmul4  30592  threehalves  30593  1mhdrd  30594  s1f1  30621  s2f1  30623  cshw1s2  30636  cycpm2tr  30763  freshmansdream  30861  lmatcl  31083  lmat22e12  31086  lmat22e21  31087  fsumcvg4  31195  oddpwdc  31614  eulerpartlems  31620  eulerpartlemb  31628  eulerpartlemt  31631  eulerpartgbij  31632  eulerpartlemmf  31635  eulerpartlemgf  31639  eulerpartlemgs2  31640  eulerpartlemn  31641  fib0  31659  fib1  31660  fibp1  31661  ofcs1  31816  signsply0  31823  signsvvf  31851  prodfzo03  31876  repr0  31884  breprexp  31906  hgt750lemd  31921  hgt750lem  31924  hgt750lem2  31925  hgt750leme  31931  tgoldbachgtde  31933  0nn0m1nnn0  32353  f1resfz0f1d  32363  usgrgt2cycl  32379  subfac0  32426  subfacval2  32436  subfaclim  32437  cvmliftlem7  32540  cvmliftlem13  32545  bccolsum  32973  fwddifn0  33627  heiborlem4  35094  heiborlem10  35100  sqn5i  39178  decpmul  39181  sqdeccom12  39182  sq3deccom12  39183  235t711  39184  ex-decpmul  39185  0prjspn  39277  nacsfix  39316  diophrw  39363  pell1qr1  39475  monotoddzzfi  39546  jm2.23  39600  hbtlem5  39735  mncn0  39746  aaitgo  39769  mon1pid  39812  brfvrcld  40043  corclrcl  40059  dfrtrcl3  40085  fvrtrcllb0d  40087  fvrtrcllb0da  40088  corcltrcl  40091  cotrclrcl  40094  k0004val0  40511  bccn0  40682  bccn1  40683  binomcxplemradcnv  40691  binomcxplemnotnn0  40695  dvnmul  42235  dvnprodlem3  42240  wallispilem2  42358  wallispi2lem2  42364  stirlinglem5  42370  stirlinglem7  42372  fourierdlem83  42481  fourierdlem112  42510  fouriersw  42523  elaa2lem  42525  elaa2  42526  etransclem48  42574  etransc  42575  iccelpart  43600  fmtno0  43709  fmtnorec2  43712  fmtno5lem1  43722  fmtno5lem2  43723  fmtno5lem4  43725  257prm  43730  fmtnofac2  43738  fmtnofac1  43739  fmtno4prmfac  43741  fmtno4nprmfac193  43743  fmtno5faclem1  43748  fmtno5faclem2  43749  fmtno5faclem3  43750  fmtno5fac  43751  fmtno5nprm  43752  139prmALT  43766  31prm  43767  127prm  43770  2exp11  43772  m11nprm  43773  bits0ALTV  43851  2exp340mod341  43905  nfermltl2rev  43915  evengpoap3  43971  tgoldbachlt  43988  tgoldbach  43989  nn0mnd  44093  ssnn0ssfz  44404  dig1  44675  0dig2nn0e  44679  0dig2nn0o  44680