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

Theorem rpssre 11226
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 11222 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3508 1  |-  RR+  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3476   RRcr 9487   RR+crp 11216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-in 3483  df-ss 3490  df-rp 11217
This theorem is referenced by:  rpred  11252  rpexpcl  12148  sqrlem3  13035  fsumrpcl  13515  o1fsum  13583  divrcnv  13620  lebnumlem2  21194  bcthlem1  21495  bcthlem5  21499  aalioulem2  22460  efcvx  22575  pilem2  22578  pilem3  22579  dvrelog  22743  relogcn  22744  logcn  22753  advlog  22760  advlogexp  22761  loglesqrt  22857  rlimcnp  23020  rlimcnp3  23022  cxplim  23026  cxp2lim  23031  cxploglim  23032  divsqrtsumo1  23038  amgmlem  23044  logexprlim  23225  chto1ub  23386  chpo1ub  23390  chpo1ubb  23391  vmadivsum  23392  vmadivsumb  23393  rpvmasumlem  23397  dchrmusum2  23404  dchrvmasumlem2  23408  dchrvmasumiflem2  23412  dchrisum0fno1  23421  rpvmasum2  23422  dchrisum0lem1  23426  dchrisum0lem2a  23427  dchrisum0lem2  23428  dchrisum0  23430  dchrmusumlem  23432  rplogsum  23437  dirith2  23438  mudivsum  23440  mulogsumlem  23441  mulogsum  23442  mulog2sumlem2  23445  mulog2sumlem3  23446  log2sumbnd  23454  selberglem1  23455  selberglem2  23456  selberg2lem  23460  selberg2  23461  pntrmax  23474  pntrsumo1  23475  selbergr  23478  pntlem3  23519  pnt2  23523  xrge0iifhom  27552  signsplypnf  28144  signsply0  28145  fprodrpcl  28662  rprisefaccl  28719  heicant  29624  totbndbnd  29886  rpexpmord  30486  seff  30792  taupilem2  36768  taupi  36769
  Copyright terms: Public domain W3C validator