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

Theorem rpssre 10380
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 10376 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3197 1  |-  RR+  C_  RR
Colors of variables: wff set class
Syntax hints:    C_ wss 3165   RRcr 8752   RR+crp 10370
This theorem is referenced by:  rpred  10406  rpexpcl  11138  sqrlem3  11746  fsumrpcl  12226  o1fsum  12287  divrcnv  12327  lebnumlem2  18476  bcthlem1  18762  bcthlem5  18766  aalioulem2  19729  efcvx  19841  pilem2  19844  pilem3  19845  dvrelog  20000  relogcn  20001  logcn  20010  advlog  20017  advlogexp  20018  loglesqr  20114  rlimcnp  20276  rlimcnp3  20278  cxplim  20282  cxp2lim  20287  cxploglim  20288  divsqrsumo1  20294  amgmlem  20300  logexprlim  20480  chto1ub  20641  chpo1ub  20645  chpo1ubb  20646  vmadivsum  20647  vmadivsumb  20648  rpvmasumlem  20652  dchrmusum2  20659  dchrvmasumlem2  20663  dchrvmasumiflem2  20667  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0  20685  dchrmusumlem  20687  rplogsum  20692  dirith2  20693  mudivsum  20695  mulogsumlem  20696  mulogsum  20697  mulog2sumlem2  20700  mulog2sumlem3  20701  log2sumbnd  20709  selberglem1  20710  selberglem2  20711  selberg2lem  20715  selberg2  20716  pntrmax  20729  pntrsumo1  20730  selbergr  20733  pntlem3  20774  pnt2  20778  xrge0iifhom  23334  totbndbnd  26616  rpexpmord  27136  seff  27641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-in 3172  df-ss 3179  df-rp 10371
  Copyright terms: Public domain W3C validator