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

Theorem rpssre 10578
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 10574 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3312 1  |-  RR+  C_  RR
Colors of variables: wff set class
Syntax hints:    C_ wss 3280   RRcr 8945   RR+crp 10568
This theorem is referenced by:  rpred  10604  rpexpcl  11355  sqrlem3  12005  fsumrpcl  12486  o1fsum  12547  divrcnv  12587  lebnumlem2  18940  bcthlem1  19230  bcthlem5  19234  aalioulem2  20203  efcvx  20318  pilem2  20321  pilem3  20322  dvrelog  20481  relogcn  20482  logcn  20491  advlog  20498  advlogexp  20499  loglesqr  20595  rlimcnp  20757  rlimcnp3  20759  cxplim  20763  cxp2lim  20768  cxploglim  20769  divsqrsumo1  20775  amgmlem  20781  logexprlim  20962  chto1ub  21123  chpo1ub  21127  chpo1ubb  21128  vmadivsum  21129  vmadivsumb  21130  rpvmasumlem  21134  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumiflem2  21149  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0  21167  dchrmusumlem  21169  rplogsum  21174  dirith2  21175  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  mulog2sumlem2  21182  mulog2sumlem3  21183  log2sumbnd  21191  selberglem1  21192  selberglem2  21193  selberg2lem  21197  selberg2  21198  pntrmax  21211  pntrsumo1  21212  selbergr  21215  pntlem3  21256  pnt2  21260  xrge0iifhom  24276  fprodrpcl  25235  rprisefaccl  25291  totbndbnd  26388  rpexpmord  26901  seff  27406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-in 3287  df-ss 3294  df-rp 10569
  Copyright terms: Public domain W3C validator