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

Theorem 0nn0 11904
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 2801 . 2 0 = 0
2 elnn0 11891 . . . 4 (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
32biimpri 231 . . 3 ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
43olcs 873 . 2 (0 = 0 → 0 ∈ ℕ0)
51, 4ax-mp 5 1 0 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wo 844   = wceq 1538  wcel 2112  0cc0 10530  cn 11629  0cn0 11889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-mulcl 10592  ax-i2m1 10598
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-n0 11890
This theorem is referenced by:  0xnn0  11965  nn0ind-raph  12074  10nn0  12108  declei  12126  numlti  12127  nummul1c  12139  decaddc2  12146  decrmanc  12147  decrmac  12148  decaddm10  12149  decaddi  12150  decaddci  12151  decaddci2  12152  decmul1  12154  decmulnc  12157  6p5e11  12163  7p4e11  12166  8p3e11  12171  9p2e11  12177  10p10e20  12185  xnn0n0n1ge2b  12518  0elfz  13003  4fvwrd4  13026  fvinim0ffz  13155  ssnn0fi  13352  fsuppmapnn0fiubex  13359  exple1  13540  nn0opth2  13632  faclbnd4lem3  13655  bc0k  13671  bcn1  13673  bccl  13682  hasheq0  13724  hashrabrsn  13733  hashbc  13811  fi1uzind  13855  brfi1ind  13857  opfi1ind  13860  iswrdi  13865  wrdnfi  13895  s1fv  13959  ccat2s1fst  13995  ccat2s1fstOLD  13996  splfv2a  14113  repsw0  14134  0csh0  14150  cshw1  14179  s2fv0  14244  s3fv0  14248  s4fv0  14252  pfx2  14304  ofs1  14325  relexp0g  14376  relexpaddg  14407  rtrclreclem1  14412  fsumnn0cl  15088  binom  15180  bcxmas  15185  isumnn0nn  15192  climcndslem1  15199  geoser  15217  geomulcvg  15227  risefac0  15376  fallfac0  15377  risefac1  15382  fallfac1  15383  binomfallfaclem2  15389  binomfallfac  15390  bpoly0  15399  bpoly2  15406  bpoly3  15407  bpoly4  15408  fsumcube  15409  ef0lem  15427  ege2le3  15438  ef4p  15461  efgt1p2  15462  efgt1p  15463  ruclem11  15588  nthruz  15601  nn0o  15727  ndvdssub  15753  bits0  15770  0bits  15781  sadcf  15795  sadc0  15796  sadcaddlem  15799  sadcadd  15800  sadadd2lem  15801  sadadd2  15802  smupf  15820  smup0  15821  smumullem  15834  gcdcl  15848  nn0seqcvgd  15907  algcvg  15913  eucalg  15924  lcmcl  15938  lcmfval  15958  lcmfcl  15965  pclem  16168  pcfac  16228  vdwap0  16305  vdwap1  16306  vdwlem6  16315  hashbc0  16334  0ram  16349  0ramcl  16352  ramz2  16353  ramz  16354  ramcl  16358  prmo0  16365  dec5dvds2  16394  2exp16  16419  11prm  16443  37prm  16449  43prm  16450  83prm  16451  139prm  16452  163prm  16453  317prm  16454  631prm  16455  1259lem1  16459  1259lem2  16460  1259lem3  16461  1259lem4  16462  1259lem5  16463  2503lem1  16465  2503lem2  16466  2503lem3  16467  2503prm  16468  4001lem1  16469  4001lem2  16470  4001lem3  16471  4001lem4  16472  4001prm  16473  odrngstr  16674  imasvalstr  16720  ipostr  17758  gsumws1  17997  cycsubm  18340  psgnunilem2  18618  psgnunilem3  18619  odfval  18655  oddvdsnn0  18667  pgp0  18716  sylow1lem1  18718  cyggex2  19013  telgsums  19109  srgbinomlem3  19288  srgbinomlem4  19289  srgbinom  19291  cnfldstr  20096  cnfldfun  20106  nn0subm  20149  expmhm  20163  nn0srg  20164  znf1o  20246  zzngim  20247  cygznlem1  20261  cygznlem2a  20262  cygznlem3  20264  cygth  20266  thlle  20389  snifpsrbag  20607  fczpsrbag  20608  psrlidm  20644  mvrf1  20666  mplcoe3  20709  mplcoe5  20711  ltbwe  20715  psrbag0  20736  psrbagsn  20737  evlslem1  20757  00ply1bas  20872  ply1plusgfvi  20874  coe1sclmul  20914  coe1sclmul2  20916  coe1scl  20919  ply1sclid  20920  ply1idvr1  20925  cply1coe0bi  20932  cpm2mf  21360  m2cpminvid2lem  21362  m2cpminvid2  21363  m2cpmfo  21364  decpmatid  21378  pmatcollpw3  21392  pmatcollpw3fi1lem1  21394  pmatcollpwscmatlem1  21397  pmatcollpwscmatlem2  21398  idpm2idmp  21409  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  cpmadugsumlemF  21484  dscmet  23182  ehl0base  24023  ehl0  24024  itgcnlem  24396  dvn0  24530  dvn1  24532  cpncn  24542  dveflem  24585  c1lip2  24604  tdeglem4  24664  deg1le0  24715  ply1divex  24740  ply1rem  24767  fta1g  24771  plyconst  24806  plypf1  24812  plyco  24841  0dgr  24845  0dgrb  24846  coefv0  24848  dgreq0  24865  vieta1lem2  24910  vieta1  24911  aareccl  24925  aannenlem2  24928  taylthlem1  24971  radcnv0  25014  abelthlem6  25034  abelthlem9  25038  logtayl  25254  cxp0  25264  cxpeq  25349  leibpilem2  25530  leibpi  25531  log2ublem3  25537  log2ub  25538  log2le1  25539  divsqrtsumlem  25568  dmgmn0  25614  lgambdd  25625  sqff1o  25770  ppiublem2  25790  chtublem  25798  bclbnd  25867  bposlem8  25878  lgsval  25888  dchrisum0flblem1  26095  dchrisum0flb  26097  ostth2lem2  26221  usgrexmplef  27052  usgr0edg0rusgr  27368  usgr2pthlem  27555  wwlksn0s  27650  rusgrnumwwlkb0  27760  erclwwlkref  27808  clwwlkf1  27837  0wlkonlem1  27906  upgr4cycl4dv4e  27973  1kp2ke3k  28234  ex-fac  28239  ex-prmo  28247  nn0min  30565  dpmul1000  30604  dp0h  30607  dpexpp1  30613  dpmul4  30619  threehalves  30620  1mhdrd  30621  s1f1  30648  s2f1  30650  cshw1s2  30663  cycpm2tr  30814  freshmansdream  30912  lmatcl  31169  lmat22e12  31172  lmat22e21  31173  fsumcvg4  31301  oddpwdc  31720  eulerpartlems  31726  eulerpartlemb  31734  eulerpartlemt  31737  eulerpartgbij  31738  eulerpartlemmf  31741  eulerpartlemgf  31745  eulerpartlemgs2  31746  eulerpartlemn  31747  fib0  31765  fib1  31766  fibp1  31767  ofcs1  31922  signsply0  31929  signsvvf  31957  prodfzo03  31982  repr0  31990  breprexp  32012  hgt750lemd  32027  hgt750lem  32030  hgt750lem2  32031  hgt750leme  32037  tgoldbachgtde  32039  0nn0m1nnn0  32459  f1resfz0f1d  32469  usgrgt2cycl  32485  subfac0  32532  subfacval2  32542  subfaclim  32543  cvmliftlem7  32646  cvmliftlem13  32651  bccolsum  33079  fwddifn0  33733  heiborlem4  35245  heiborlem10  35251  12gcd5e1  39284  60gcd6e6  39285  60gcd7e1  39286  420gcd8e4  39287  12lcm5e60  39289  60lcm7e420  39291  420lcm8e840  39292  lcmineqlem  39333  3lexlogpow5ineq1  39334  sqn5i  39466  decpmul  39469  sqdeccom12  39470  sq3deccom12  39471  235t711  39472  ex-decpmul  39473  0prjspn  39601  nacsfix  39640  diophrw  39687  pell1qr1  39799  monotoddzzfi  39870  jm2.23  39924  hbtlem5  40059  mncn0  40070  aaitgo  40093  mon1pid  40136  brfvrcld  40379  corclrcl  40395  dfrtrcl3  40421  fvrtrcllb0d  40423  fvrtrcllb0da  40424  corcltrcl  40427  cotrclrcl  40430  k0004val0  40844  bccn0  41034  bccn1  41035  binomcxplemradcnv  41043  binomcxplemnotnn0  41047  dvnmul  42572  dvnprodlem3  42577  wallispilem2  42695  wallispi2lem2  42701  stirlinglem5  42707  stirlinglem7  42709  fourierdlem83  42818  fourierdlem112  42847  fouriersw  42860  elaa2lem  42862  elaa2  42863  etransclem48  42911  etransc  42912  iccelpart  43937  fmtno0  44044  fmtnorec2  44047  fmtno5lem1  44057  fmtno5lem2  44058  fmtno5lem4  44060  257prm  44065  fmtnofac2  44073  fmtnofac1  44074  fmtno4prmfac  44076  fmtno4nprmfac193  44078  fmtno5faclem1  44083  fmtno5faclem2  44084  fmtno5faclem3  44085  fmtno5fac  44086  fmtno5nprm  44087  139prmALT  44100  31prm  44101  127prm  44103  2exp11  44105  m11nprm  44106  bits0ALTV  44184  2exp340mod341  44238  nfermltl2rev  44248  evengpoap3  44304  tgoldbachlt  44321  tgoldbach  44322  nn0mnd  44426  ssnn0ssfz  44738  dig1  45009  0dig2nn0e  45013  0dig2nn0o  45014  0aryfvalel  45035  itcoval0  45063  itcoval1  45064  ackval0  45081  ackval1  45082  ackvalsuc0val  45088  ackval0012  45090  ackval1012  45091  ackval2012  45092  ackval3012  45093  ackval41a  45095
  Copyright terms: Public domain W3C validator