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

Theorem rpssre 10993
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 10989 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3355 1  |-  RR+  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3323   RRcr 9273   RR+crp 10983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-in 3330  df-ss 3337  df-rp 10984
This theorem is referenced by:  rpred  11019  rpexpcl  11876  sqrlem3  12726  fsumrpcl  13206  o1fsum  13268  divrcnv  13307  lebnumlem2  20514  bcthlem1  20815  bcthlem5  20819  aalioulem2  21779  efcvx  21894  pilem2  21897  pilem3  21898  dvrelog  22062  relogcn  22063  logcn  22072  advlog  22079  advlogexp  22080  loglesqr  22176  rlimcnp  22339  rlimcnp3  22341  cxplim  22345  cxp2lim  22350  cxploglim  22351  divsqrsumo1  22357  amgmlem  22363  logexprlim  22544  chto1ub  22705  chpo1ub  22709  chpo1ubb  22710  vmadivsum  22711  vmadivsumb  22712  rpvmasumlem  22716  dchrmusum2  22723  dchrvmasumlem2  22727  dchrvmasumiflem2  22731  dchrisum0fno1  22740  rpvmasum2  22741  dchrisum0lem1  22745  dchrisum0lem2a  22746  dchrisum0lem2  22747  dchrisum0  22749  dchrmusumlem  22751  rplogsum  22756  dirith2  22757  mudivsum  22759  mulogsumlem  22760  mulogsum  22761  mulog2sumlem2  22764  mulog2sumlem3  22765  log2sumbnd  22773  selberglem1  22774  selberglem2  22775  selberg2lem  22779  selberg2  22780  pntrmax  22793  pntrsumo1  22794  selbergr  22797  pntlem3  22838  pnt2  22842  xrge0iifhom  26336  signsplypnf  26920  signsply0  26921  fprodrpcl  27438  rprisefaccl  27495  heicant  28397  totbndbnd  28659  rpexpmord  29260  seff  29566  taupilem2  35509  taupi  35510
  Copyright terms: Public domain W3C validator