MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0nn0 Structured version   Visualization version   GIF version

Theorem 0nn0 11900
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
0nn0 0 ∈ ℕ0

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2818 . 2 0 = 0
2 elnn0 11887 . . . 4 (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
32biimpri 229 . . 3 ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
43olcs 872 . 2 (0 = 0 → 0 ∈ ℕ0)
51, 4ax-mp 5 1 0 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wo 841   = wceq 1528  wcel 2105  0cc0 10525  cn 11626  0cn0 11885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-i2m1 10593
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-sn 4558  df-n0 11886
This theorem is referenced by:  0xnn0  11961  nn0ind-raph  12070  10nn0  12104  declei  12122  numlti  12123  nummul1c  12135  decaddc2  12142  decrmanc  12143  decrmac  12144  decaddm10  12145  decaddi  12146  decaddci  12147  decaddci2  12148  decmul1  12150  decmulnc  12153  6p5e11  12159  7p4e11  12162  8p3e11  12167  9p2e11  12173  10p10e20  12181  xnn0n0n1ge2b  12514  0elfz  12992  4fvwrd4  13015  fvinim0ffz  13144  ssnn0fi  13341  fsuppmapnn0fiubex  13348  exple1  13528  nn0opth2  13620  faclbnd4lem3  13643  bc0k  13659  bcn1  13661  bccl  13670  hasheq0  13712  hashrabrsn  13721  hashbc  13799  fi1uzind  13843  brfi1ind  13845  opfi1ind  13848  iswrdi  13853  wrdnfi  13887  s1fv  13952  ccat2s1fst  13988  ccat2s1fstOLD  13989  splfv2a  14106  repsw0  14127  0csh0  14143  cshw1  14172  s2fv0  14237  s3fv0  14241  s4fv0  14245  pfx2  14297  ofs1  14318  relexp0g  14369  relexpaddg  14400  rtrclreclem1  14405  fsumnn0cl  15081  binom  15173  bcxmas  15178  isumnn0nn  15185  climcndslem1  15192  geoser  15210  geomulcvg  15220  risefac0  15369  fallfac0  15370  risefac1  15375  fallfac1  15376  binomfallfaclem2  15382  binomfallfac  15383  bpoly0  15392  bpoly2  15399  bpoly3  15400  bpoly4  15401  fsumcube  15402  ef0lem  15420  ege2le3  15431  ef4p  15454  efgt1p2  15455  efgt1p  15456  ruclem11  15581  nthruz  15594  nn0o  15722  ndvdssub  15748  bits0  15765  0bits  15776  sadcf  15790  sadc0  15791  sadcaddlem  15794  sadcadd  15795  sadadd2lem  15796  sadadd2  15797  smupf  15815  smup0  15816  smumullem  15829  gcdcl  15843  nn0seqcvgd  15902  algcvg  15908  eucalg  15919  lcmcl  15933  lcmfval  15953  lcmfcl  15960  pclem  16163  pcfac  16223  vdwap0  16300  vdwap1  16301  vdwlem6  16310  hashbc0  16329  0ram  16344  0ramcl  16347  ramz2  16348  ramz  16349  ramcl  16353  prmo0  16360  dec5dvds2  16389  2exp16  16412  11prm  16436  37prm  16442  43prm  16443  83prm  16444  139prm  16445  163prm  16446  317prm  16447  631prm  16448  1259lem1  16452  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  2503lem1  16458  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  4001prm  16466  odrngstr  16667  imasvalstr  16713  ipostr  17751  gsumws1  17990  cycsubm  18283  psgnunilem2  18552  psgnunilem3  18553  odfval  18589  oddvdsnn0  18601  pgp0  18650  sylow1lem1  18652  cyggex2  18946  telgsums  19042  srgbinomlem3  19221  srgbinomlem4  19222  srgbinom  19224  snifpsrbag  20074  fczpsrbag  20075  psrlidm  20111  mvrf1  20133  mplcoe3  20175  mplcoe5  20177  ltbwe  20181  psrbag0  20202  psrbagsn  20203  evlslem1  20223  00ply1bas  20336  ply1plusgfvi  20338  coe1sclmul  20378  coe1sclmul2  20380  coe1scl  20383  ply1sclid  20384  ply1idvr1  20389  cply1coe0bi  20396  cnfldstr  20475  cnfldfun  20485  nn0subm  20528  expmhm  20542  nn0srg  20543  znf1o  20626  zzngim  20627  cygznlem1  20641  cygznlem2a  20642  cygznlem3  20644  cygth  20646  thlle  20769  cpm2mf  21288  m2cpminvid2lem  21290  m2cpminvid2  21291  m2cpmfo  21292  decpmatid  21306  pmatcollpw3  21320  pmatcollpw3fi1lem1  21322  pmatcollpwscmatlem1  21325  pmatcollpwscmatlem2  21326  idpm2idmp  21337  chfacfscmulgsum  21396  chfacfpmmulgsum  21400  cpmadugsumlemF  21412  dscmet  23109  ehl0base  23946  ehl0  23947  itgcnlem  24317  dvn0  24448  dvn1  24450  cpncn  24460  dveflem  24503  c1lip2  24522  tdeglem4  24581  deg1le0  24632  ply1divex  24657  ply1rem  24684  fta1g  24688  plyconst  24723  plypf1  24729  plyco  24758  0dgr  24762  0dgrb  24763  coefv0  24765  dgreq0  24782  vieta1lem2  24827  vieta1  24828  aareccl  24842  aannenlem2  24845  taylthlem1  24888  radcnv0  24931  abelthlem6  24951  abelthlem9  24955  logtayl  25170  cxp0  25180  cxpeq  25265  leibpilem2  25446  leibpi  25447  log2ublem3  25453  log2ub  25454  log2le1  25455  divsqrtsumlem  25484  dmgmn0  25530  lgambdd  25541  sqff1o  25686  ppiublem2  25706  chtublem  25714  bclbnd  25783  bposlem8  25794  lgsval  25804  dchrisum0flblem1  26011  dchrisum0flb  26013  ostth2lem2  26137  usgrexmplef  26968  usgr0edg0rusgr  27284  usgr2pthlem  27471  wwlksn0s  27566  rusgrnumwwlkb0  27677  erclwwlkref  27725  clwwlkf1  27755  0wlkonlem1  27824  upgr4cycl4dv4e  27891  1kp2ke3k  28152  ex-fac  28157  ex-prmo  28165  nn0min  30463  dpmul1000  30502  dp0h  30505  dpexpp1  30511  dpmul4  30517  threehalves  30518  1mhdrd  30519  s1f1  30546  s2f1  30548  cshw1s2  30561  cycpm2tr  30688  freshmansdream  30786  lmatcl  30980  lmat22e12  30983  lmat22e21  30984  fsumcvg4  31092  oddpwdc  31511  eulerpartlems  31517  eulerpartlemb  31525  eulerpartlemt  31528  eulerpartgbij  31529  eulerpartlemmf  31532  eulerpartlemgf  31536  eulerpartlemgs2  31537  eulerpartlemn  31538  fib0  31556  fib1  31557  fibp1  31558  ofcs1  31713  signsply0  31720  signsvvf  31748  prodfzo03  31773  repr0  31781  breprexp  31803  hgt750lemd  31818  hgt750lem  31821  hgt750lem2  31822  hgt750leme  31828  tgoldbachgtde  31830  0nn0m1nnn0  32248  f1resfz0f1d  32258  usgrgt2cycl  32274  subfac0  32321  subfacval2  32331  subfaclim  32332  cvmliftlem7  32435  cvmliftlem13  32440  bccolsum  32868  fwddifn0  33522  heiborlem4  34973  heiborlem10  34979  sqn5i  39049  decpmul  39052  sqdeccom12  39053  sq3deccom12  39054  235t711  39055  ex-decpmul  39056  0prjspn  39148  nacsfix  39187  diophrw  39234  pell1qr1  39346  monotoddzzfi  39417  jm2.23  39471  hbtlem5  39606  mncn0  39617  aaitgo  39640  mon1pid  39683  brfvrcld  39914  corclrcl  39930  dfrtrcl3  39956  fvrtrcllb0d  39958  fvrtrcllb0da  39959  corcltrcl  39962  cotrclrcl  39965  k0004val0  40382  bccn0  40552  bccn1  40553  binomcxplemradcnv  40561  binomcxplemnotnn0  40565  dvnmul  42104  dvnprodlem3  42109  wallispilem2  42228  wallispi2lem2  42234  stirlinglem5  42240  stirlinglem7  42242  fourierdlem83  42351  fourierdlem112  42380  fouriersw  42393  elaa2lem  42395  elaa2  42396  etransclem48  42444  etransc  42445  iccelpart  43470  fmtno0  43579  fmtnorec2  43582  fmtno5lem1  43592  fmtno5lem2  43593  fmtno5lem4  43595  257prm  43600  fmtnofac2  43608  fmtnofac1  43609  fmtno4prmfac  43611  fmtno4nprmfac193  43613  fmtno5faclem1  43618  fmtno5faclem2  43619  fmtno5faclem3  43620  fmtno5fac  43621  fmtno5nprm  43622  139prmALT  43636  31prm  43637  127prm  43640  2exp11  43642  m11nprm  43643  bits0ALTV  43721  2exp340mod341  43775  nfermltl2rev  43785  evengpoap3  43841  tgoldbachlt  43858  tgoldbach  43859  nn0mnd  43963  ssnn0ssfz  44325  dig1  44596  0dig2nn0e  44600  0dig2nn0o  44601
  Copyright terms: Public domain W3C validator