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

Theorem rpssre 11259
Description: The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
Assertion
Ref Expression
rpssre

Proof of Theorem rpssre
StepHypRef Expression
1 rpre 11255 . 2
21ssriv 3507 1
Colors of variables: wff setvar class
Syntax hints:  C_wss 3475   cr 9512   crp 11249
This theorem is referenced by:  rpred  11285  rpexpcl  12185  sqrlem3  13078  fsumrpcl  13559  o1fsum  13627  divrcnv  13664  fprodrpcl  13763  lebnumlem2  21462  bcthlem1  21763  bcthlem5  21767  aalioulem2  22729  efcvx  22844  pilem2  22847  pilem3  22848  dvrelog  23018  relogcn  23019  logcn  23028  advlog  23035  advlogexp  23036  loglesqrt  23132  rlimcnp  23295  rlimcnp3  23297  cxplim  23301  cxp2lim  23306  cxploglim  23307  divsqrtsumo1  23313  amgmlem  23319  logexprlim  23500  chto1ub  23661  chpo1ub  23665  chpo1ubb  23666  vmadivsum  23667  vmadivsumb  23668  rpvmasumlem  23672  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumiflem2  23687  dchrisum0fno1  23696  rpvmasum2  23697  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0  23705  dchrmusumlem  23707  rplogsum  23712  dirith2  23713  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  mulog2sumlem2  23720  mulog2sumlem3  23721  log2sumbnd  23729  selberglem1  23730  selberglem2  23731  selberg2lem  23735  selberg2  23736  pntrmax  23749  pntrsumo1  23750  selbergr  23753  pntlem3  23794  pnt2  23798  xrge0iifhom  27919  signsplypnf  28507  signsply0  28508  rprisefaccl  29145  heicant  30049  totbndbnd  30285  rpexpmord  30884  seff  31189  taupilem2  37697  taupi  37698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3482  df-ss 3489  df-rp 11250
  Copyright terms: Public domain W3C validator