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

Theorem 0nn0 11901
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 2821 . 2 0 = 0
2 elnn0 11888 . . . 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 10526  cn 11627  0cn0 11886
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 2793  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-i2m1 10594
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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3940  df-sn 4560  df-n0 11887
This theorem is referenced by:  0xnn0  11962  nn0ind-raph  12071  10nn0  12105  declei  12123  numlti  12124  nummul1c  12136  decaddc2  12143  decrmanc  12144  decrmac  12145  decaddm10  12146  decaddi  12147  decaddci  12148  decaddci2  12149  decmul1  12151  decmulnc  12154  6p5e11  12160  7p4e11  12163  8p3e11  12168  9p2e11  12174  10p10e20  12182  xnn0n0n1ge2b  12516  0elfz  12994  4fvwrd4  13017  fvinim0ffz  13146  ssnn0fi  13343  fsuppmapnn0fiubex  13350  exple1  13530  nn0opth2  13622  faclbnd4lem3  13645  bc0k  13661  bcn1  13663  bccl  13672  hasheq0  13714  hashrabrsn  13723  hashbc  13801  fi1uzind  13845  brfi1ind  13847  opfi1ind  13850  iswrdi  13855  wrdnfi  13889  s1fv  13954  ccat2s1fst  13990  ccat2s1fstOLD  13991  splfv2a  14108  repsw0  14129  0csh0  14145  cshw1  14174  s2fv0  14239  s3fv0  14243  s4fv0  14247  pfx2  14299  ofs1  14320  relexp0g  14371  relexpaddg  14402  rtrclreclem1  14407  fsumnn0cl  15083  binom  15175  bcxmas  15180  isumnn0nn  15187  climcndslem1  15194  geoser  15212  geomulcvg  15222  risefac0  15371  fallfac0  15372  risefac1  15377  fallfac1  15378  binomfallfaclem2  15384  binomfallfac  15385  bpoly0  15394  bpoly2  15401  bpoly3  15402  bpoly4  15403  fsumcube  15404  ef0lem  15422  ege2le3  15433  ef4p  15456  efgt1p2  15457  efgt1p  15458  ruclem11  15583  nthruz  15596  nn0o  15724  ndvdssub  15750  bits0  15767  0bits  15778  sadcf  15792  sadc0  15793  sadcaddlem  15796  sadcadd  15797  sadadd2lem  15798  sadadd2  15799  smupf  15817  smup0  15818  smumullem  15831  gcdcl  15845  nn0seqcvgd  15904  algcvg  15910  eucalg  15921  lcmcl  15935  lcmfval  15955  lcmfcl  15962  pclem  16165  pcfac  16225  vdwap0  16302  vdwap1  16303  vdwlem6  16312  hashbc0  16331  0ram  16346  0ramcl  16349  ramz2  16350  ramz  16351  ramcl  16355  prmo0  16362  dec5dvds2  16391  2exp16  16414  11prm  16438  37prm  16444  43prm  16445  83prm  16446  139prm  16447  163prm  16448  317prm  16449  631prm  16450  1259lem1  16454  1259lem2  16455  1259lem3  16456  1259lem4  16457  1259lem5  16458  2503lem1  16460  2503lem2  16461  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  4001prm  16468  odrngstr  16669  imasvalstr  16715  ipostr  17753  gsumws1  17992  cycsubm  18285  psgnunilem2  18554  psgnunilem3  18555  odfval  18591  oddvdsnn0  18603  pgp0  18652  sylow1lem1  18654  cyggex2  18948  telgsums  19044  srgbinomlem3  19223  srgbinomlem4  19224  srgbinom  19226  snifpsrbag  20076  fczpsrbag  20077  psrlidm  20113  mvrf1  20135  mplcoe3  20177  mplcoe5  20179  ltbwe  20183  psrbag0  20204  psrbagsn  20205  evlslem1  20225  00ply1bas  20338  ply1plusgfvi  20340  coe1sclmul  20380  coe1sclmul2  20382  coe1scl  20385  ply1sclid  20386  ply1idvr1  20391  cply1coe0bi  20398  cnfldstr  20477  cnfldfun  20487  nn0subm  20530  expmhm  20544  nn0srg  20545  znf1o  20628  zzngim  20629  cygznlem1  20643  cygznlem2a  20644  cygznlem3  20646  cygth  20648  thlle  20771  cpm2mf  21290  m2cpminvid2lem  21292  m2cpminvid2  21293  m2cpmfo  21294  decpmatid  21308  pmatcollpw3  21322  pmatcollpw3fi1lem1  21324  pmatcollpwscmatlem1  21327  pmatcollpwscmatlem2  21328  idpm2idmp  21339  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  cpmadugsumlemF  21414  dscmet  23111  ehl0base  23948  ehl0  23949  itgcnlem  24319  dvn0  24450  dvn1  24452  cpncn  24462  dveflem  24505  c1lip2  24524  tdeglem4  24583  deg1le0  24634  ply1divex  24659  ply1rem  24686  fta1g  24690  plyconst  24725  plypf1  24731  plyco  24760  0dgr  24764  0dgrb  24765  coefv0  24767  dgreq0  24784  vieta1lem2  24829  vieta1  24830  aareccl  24844  aannenlem2  24847  taylthlem1  24890  radcnv0  24933  abelthlem6  24953  abelthlem9  24957  logtayl  25170  cxp0  25180  cxpeq  25265  leibpilem2  25447  leibpi  25448  log2ublem3  25454  log2ub  25455  log2le1  25456  divsqrtsumlem  25485  dmgmn0  25531  lgambdd  25542  sqff1o  25687  ppiublem2  25707  chtublem  25715  bclbnd  25784  bposlem8  25795  lgsval  25805  dchrisum0flblem1  26012  dchrisum0flb  26014  ostth2lem2  26138  usgrexmplef  26969  usgr0edg0rusgr  27285  usgr2pthlem  27472  wwlksn0s  27567  rusgrnumwwlkb0  27678  erclwwlkref  27726  clwwlkf1  27756  0wlkonlem1  27825  upgr4cycl4dv4e  27892  1kp2ke3k  28153  ex-fac  28158  ex-prmo  28166  nn0min  30464  dpmul1000  30503  dp0h  30506  dpexpp1  30512  dpmul4  30518  threehalves  30519  1mhdrd  30520  s1f1  30547  s2f1  30549  cshw1s2  30562  cycpm2tr  30689  freshmansdream  30787  lmatcl  30981  lmat22e12  30984  lmat22e21  30985  fsumcvg4  31093  oddpwdc  31512  eulerpartlems  31518  eulerpartlemb  31526  eulerpartlemt  31529  eulerpartgbij  31530  eulerpartlemmf  31533  eulerpartlemgf  31537  eulerpartlemgs2  31538  eulerpartlemn  31539  fib0  31557  fib1  31558  fibp1  31559  ofcs1  31714  signsply0  31721  signsvvf  31749  prodfzo03  31774  repr0  31782  breprexp  31804  hgt750lemd  31819  hgt750lem  31822  hgt750lem2  31823  hgt750leme  31829  tgoldbachgtde  31831  0nn0m1nnn0  32249  f1resfz0f1d  32259  usgrgt2cycl  32275  subfac0  32322  subfacval2  32332  subfaclim  32333  cvmliftlem7  32436  cvmliftlem13  32441  bccolsum  32869  fwddifn0  33523  heiborlem4  34975  heiborlem10  34981  sqn5i  39051  decpmul  39054  sqdeccom12  39055  sq3deccom12  39056  235t711  39057  ex-decpmul  39058  0prjspn  39150  nacsfix  39189  diophrw  39236  pell1qr1  39348  monotoddzzfi  39419  jm2.23  39473  hbtlem5  39608  mncn0  39619  aaitgo  39642  mon1pid  39685  brfvrcld  39916  corclrcl  39932  dfrtrcl3  39958  fvrtrcllb0d  39960  fvrtrcllb0da  39961  corcltrcl  39964  cotrclrcl  39967  k0004val0  40384  bccn0  40555  bccn1  40556  binomcxplemradcnv  40564  binomcxplemnotnn0  40568  dvnmul  42108  dvnprodlem3  42113  wallispilem2  42232  wallispi2lem2  42238  stirlinglem5  42244  stirlinglem7  42246  fourierdlem83  42355  fourierdlem112  42384  fouriersw  42397  elaa2lem  42399  elaa2  42400  etransclem48  42448  etransc  42449  iccelpart  43440  fmtno0  43549  fmtnorec2  43552  fmtno5lem1  43562  fmtno5lem2  43563  fmtno5lem4  43565  257prm  43570  fmtnofac2  43578  fmtnofac1  43579  fmtno4prmfac  43581  fmtno4nprmfac193  43583  fmtno5faclem1  43588  fmtno5faclem2  43589  fmtno5faclem3  43590  fmtno5fac  43591  fmtno5nprm  43592  139prmALT  43606  31prm  43607  127prm  43610  2exp11  43612  m11nprm  43613  bits0ALTV  43691  2exp340mod341  43745  nfermltl2rev  43755  evengpoap3  43811  tgoldbachlt  43828  tgoldbach  43829  nn0mnd  43933  ssnn0ssfz  44295  dig1  44566  0dig2nn0e  44570  0dig2nn0o  44571
  Copyright terms: Public domain W3C validator