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

Theorem rpssre 11277
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 11273 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3448 1  |-  RR+  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3416   RRcr 9523   RR+crp 11267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rab 2765  df-in 3423  df-ss 3430  df-rp 11268
This theorem is referenced by:  rpred  11306  rpexpcl  12231  sqrlem3  13229  fsumrpcl  13710  o1fsum  13780  divrcnv  13817  fprodrpcl  13917  rprisefaccl  13970  lebnumlem2  21756  bcthlem1  22057  bcthlem5  22061  aalioulem2  23023  efcvx  23138  pilem2  23141  pilem3  23142  dvrelog  23314  relogcn  23315  logcn  23324  advlog  23331  advlogexp  23332  loglesqrt  23430  rlimcnp  23623  rlimcnp3  23625  cxplim  23629  cxp2lim  23634  cxploglim  23635  divsqrtsumo1  23641  amgmlem  23647  logexprlim  23883  chto1ub  24044  chpo1ub  24048  chpo1ubb  24049  vmadivsum  24050  vmadivsumb  24051  rpvmasumlem  24055  dchrmusum2  24062  dchrvmasumlem2  24066  dchrvmasumiflem2  24070  dchrisum0fno1  24079  rpvmasum2  24080  dchrisum0lem1  24084  dchrisum0lem2a  24085  dchrisum0lem2  24086  dchrisum0  24088  dchrmusumlem  24090  rplogsum  24095  dirith2  24096  mudivsum  24098  mulogsumlem  24099  mulogsum  24100  mulog2sumlem2  24103  mulog2sumlem3  24104  log2sumbnd  24112  selberglem1  24113  selberglem2  24114  selberg2lem  24118  selberg2  24119  pntrmax  24132  pntrsumo1  24133  selbergr  24136  pntlem3  24177  pnt2  24181  xrge0iifhom  28385  omssubadd  28761  signsplypnf  29026  signsply0  29027  taupilem2  31261  taupi  31262  heicant  31434  totbndbnd  31580  rpexpmord  35258  seff  36050  elbigolo1  38701
  Copyright terms: Public domain W3C validator