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

Theorem rpssre 10989
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 10985 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3348 1  |-  RR+  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3316   RRcr 9269   RR+crp 10979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-in 3323  df-ss 3330  df-rp 10980
This theorem is referenced by:  rpred  11015  rpexpcl  11868  sqrlem3  12718  fsumrpcl  13198  o1fsum  13259  divrcnv  13298  lebnumlem2  20376  bcthlem1  20677  bcthlem5  20681  aalioulem2  21684  efcvx  21799  pilem2  21802  pilem3  21803  dvrelog  21967  relogcn  21968  logcn  21977  advlog  21984  advlogexp  21985  loglesqr  22081  rlimcnp  22244  rlimcnp3  22246  cxplim  22250  cxp2lim  22255  cxploglim  22256  divsqrsumo1  22262  amgmlem  22268  logexprlim  22449  chto1ub  22610  chpo1ub  22614  chpo1ubb  22615  vmadivsum  22616  vmadivsumb  22617  rpvmasumlem  22621  dchrmusum2  22628  dchrvmasumlem2  22632  dchrvmasumiflem2  22636  dchrisum0fno1  22645  rpvmasum2  22646  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0  22654  dchrmusumlem  22656  rplogsum  22661  dirith2  22662  mudivsum  22664  mulogsumlem  22665  mulogsum  22666  mulog2sumlem2  22669  mulog2sumlem3  22670  log2sumbnd  22678  selberglem1  22679  selberglem2  22680  selberg2lem  22684  selberg2  22685  pntrmax  22698  pntrsumo1  22699  selbergr  22702  pntlem3  22743  pnt2  22747  xrge0iifhom  26221  signsplypnf  26799  signsply0  26800  fprodrpcl  27316  rprisefaccl  27373  heicant  28270  totbndbnd  28532  rpexpmord  29134  seff  29440  taupilem2  35189  taupi  35190
  Copyright terms: Public domain W3C validator