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

Theorem rpssre 10364
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 10360 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3184 1  |-  RR+  C_  RR
Colors of variables: wff set class
Syntax hints:    C_ wss 3152   RRcr 8736   RR+crp 10354
This theorem is referenced by:  rpred  10390  rpexpcl  11122  sqrlem3  11730  fsumrpcl  12210  o1fsum  12271  divrcnv  12311  lebnumlem2  18460  bcthlem1  18746  bcthlem5  18750  aalioulem2  19713  efcvx  19825  pilem2  19828  pilem3  19829  dvrelog  19984  relogcn  19985  logcn  19994  advlog  20001  advlogexp  20002  loglesqr  20098  rlimcnp  20260  rlimcnp3  20262  cxplim  20266  cxp2lim  20271  cxploglim  20272  divsqrsumo1  20278  amgmlem  20284  logexprlim  20464  chto1ub  20625  chpo1ub  20629  chpo1ubb  20630  vmadivsum  20631  vmadivsumb  20632  rpvmasumlem  20636  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumiflem2  20651  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0  20669  dchrmusumlem  20671  rplogsum  20676  dirith2  20677  mudivsum  20679  mulogsumlem  20680  mulogsum  20681  mulog2sumlem2  20684  mulog2sumlem3  20685  log2sumbnd  20693  selberglem1  20694  selberglem2  20695  selberg2lem  20699  selberg2  20700  pntrmax  20713  pntrsumo1  20714  selbergr  20717  pntlem3  20758  pnt2  20762  xrge0iifhom  23319  totbndbnd  26513  rpexpmord  27033  seff  27538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-in 3159  df-ss 3166  df-rp 10355
  Copyright terms: Public domain W3C validator