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

Theorem rpssre 10624
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 10620 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3354 1  |-  RR+  C_  RR
Colors of variables: wff set class
Syntax hints:    C_ wss 3322   RRcr 8991   RR+crp 10614
This theorem is referenced by:  rpred  10650  rpexpcl  11402  sqrlem3  12052  fsumrpcl  12533  o1fsum  12594  divrcnv  12634  lebnumlem2  18989  bcthlem1  19279  bcthlem5  19283  aalioulem2  20252  efcvx  20367  pilem2  20370  pilem3  20371  dvrelog  20530  relogcn  20531  logcn  20540  advlog  20547  advlogexp  20548  loglesqr  20644  rlimcnp  20806  rlimcnp3  20808  cxplim  20812  cxp2lim  20817  cxploglim  20818  divsqrsumo1  20824  amgmlem  20830  logexprlim  21011  chto1ub  21172  chpo1ub  21176  chpo1ubb  21177  vmadivsum  21178  vmadivsumb  21179  rpvmasumlem  21183  dchrmusum2  21190  dchrvmasumlem2  21194  dchrvmasumiflem2  21198  dchrisum0fno1  21207  rpvmasum2  21208  dchrisum0lem1  21212  dchrisum0lem2a  21213  dchrisum0lem2  21214  dchrisum0  21216  dchrmusumlem  21218  rplogsum  21223  dirith2  21224  mudivsum  21226  mulogsumlem  21227  mulogsum  21228  mulog2sumlem2  21231  mulog2sumlem3  21232  log2sumbnd  21240  selberglem1  21241  selberglem2  21242  selberg2lem  21246  selberg2  21247  pntrmax  21260  pntrsumo1  21261  selbergr  21264  pntlem3  21305  pnt2  21309  xrge0iifhom  24325  fprodrpcl  25284  rprisefaccl  25341  totbndbnd  26500  rpexpmord  27013  seff  27517
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-in 3329  df-ss 3336  df-rp 10615
  Copyright terms: Public domain W3C validator