MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpssre Structured version   Unicode version

Theorem rpssre 11241
Description: The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
Assertion
Ref Expression
rpssre  |-  RR+  C_  RR

Proof of Theorem rpssre
StepHypRef Expression
1 rpre 11237 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3493 1  |-  RR+  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3461   RRcr 9494   RR+crp 11231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-in 3468  df-ss 3475  df-rp 11232
This theorem is referenced by:  rpred  11267  rpexpcl  12167  sqrlem3  13060  fsumrpcl  13541  o1fsum  13609  divrcnv  13646  fprodrpcl  13745  lebnumlem2  21440  bcthlem1  21741  bcthlem5  21745  aalioulem2  22707  efcvx  22822  pilem2  22825  pilem3  22826  dvrelog  22996  relogcn  22997  logcn  23006  advlog  23013  advlogexp  23014  loglesqrt  23110  rlimcnp  23273  rlimcnp3  23275  cxplim  23279  cxp2lim  23284  cxploglim  23285  divsqrtsumo1  23291  amgmlem  23297  logexprlim  23478  chto1ub  23639  chpo1ub  23643  chpo1ubb  23644  vmadivsum  23645  vmadivsumb  23646  rpvmasumlem  23650  dchrmusum2  23657  dchrvmasumlem2  23661  dchrvmasumiflem2  23665  dchrisum0fno1  23674  rpvmasum2  23675  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0lem2  23681  dchrisum0  23683  dchrmusumlem  23685  rplogsum  23690  dirith2  23691  mudivsum  23693  mulogsumlem  23694  mulogsum  23695  mulog2sumlem2  23698  mulog2sumlem3  23699  log2sumbnd  23707  selberglem1  23708  selberglem2  23709  selberg2lem  23713  selberg2  23714  pntrmax  23727  pntrsumo1  23728  selbergr  23731  pntlem3  23772  pnt2  23776  xrge0iifhom  27897  signsplypnf  28485  signsply0  28486  rprisefaccl  29121  heicant  30025  totbndbnd  30261  rpexpmord  30860  seff  31165  taupilem2  37572  taupi  37573
  Copyright terms: Public domain W3C validator