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

Theorem rpssre 11111
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 11107 . 2  |-  ( x  e.  RR+  ->  x  e.  RR )
21ssriv 3467 1  |-  RR+  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3435   RRcr 9391   RR+crp 11101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2807  df-in 3442  df-ss 3449  df-rp 11102
This theorem is referenced by:  rpred  11137  rpexpcl  12000  sqrlem3  12851  fsumrpcl  13331  o1fsum  13393  divrcnv  13432  lebnumlem2  20665  bcthlem1  20966  bcthlem5  20970  aalioulem2  21931  efcvx  22046  pilem2  22049  pilem3  22050  dvrelog  22214  relogcn  22215  logcn  22224  advlog  22231  advlogexp  22232  loglesqr  22328  rlimcnp  22491  rlimcnp3  22493  cxplim  22497  cxp2lim  22502  cxploglim  22503  divsqrsumo1  22509  amgmlem  22515  logexprlim  22696  chto1ub  22857  chpo1ub  22861  chpo1ubb  22862  vmadivsum  22863  vmadivsumb  22864  rpvmasumlem  22868  dchrmusum2  22875  dchrvmasumlem2  22879  dchrvmasumiflem2  22883  dchrisum0fno1  22892  rpvmasum2  22893  dchrisum0lem1  22897  dchrisum0lem2a  22898  dchrisum0lem2  22899  dchrisum0  22901  dchrmusumlem  22903  rplogsum  22908  dirith2  22909  mudivsum  22911  mulogsumlem  22912  mulogsum  22913  mulog2sumlem2  22916  mulog2sumlem3  22917  log2sumbnd  22925  selberglem1  22926  selberglem2  22927  selberg2lem  22931  selberg2  22932  pntrmax  22945  pntrsumo1  22946  selbergr  22949  pntlem3  22990  pnt2  22994  xrge0iifhom  26511  signsplypnf  27094  signsply0  27095  fprodrpcl  27612  rprisefaccl  27669  heicant  28573  totbndbnd  28835  rpexpmord  29436  seff  29742  taupilem2  35939  taupi  35940
  Copyright terms: Public domain W3C validator