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

Theorem rpssre 11678
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 11674 . 2 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
21ssriv 3572 1 + ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3540  cr 9792  +crp 11667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-rp 11668
This theorem is referenced by:  rpred  11707  rpexpcl  12699  sqrlem3  13782  fsumrpcl  14264  o1fsum  14335  divrcnv  14372  fprodrpcl  14474  rprisefaccl  14542  lebnumlem2  22517  bcthlem1  22874  bcthlem5  22878  aalioulem2  23837  efcvx  23952  pilem2  23955  pilem3  23956  dvrelog  24128  relogcn  24129  logcn  24138  advlog  24145  advlogexp  24146  loglesqrt  24244  rlimcnp  24437  rlimcnp3  24439  cxplim  24443  cxp2lim  24448  cxploglim  24449  divsqrtsumo1  24455  amgmlem  24461  logexprlim  24695  chto1ub  24910  chpo1ub  24914  chpo1ubb  24915  vmadivsum  24916  vmadivsumb  24917  rpvmasumlem  24921  dchrmusum2  24928  dchrvmasumlem2  24932  dchrvmasumiflem2  24936  dchrisum0fno1  24945  rpvmasum2  24946  dchrisum0lem1  24950  dchrisum0lem2a  24951  dchrisum0lem2  24952  dchrisum0  24954  dchrmusumlem  24956  rplogsum  24961  dirith2  24962  mudivsum  24964  mulogsumlem  24965  mulogsum  24966  mulog2sumlem2  24969  mulog2sumlem3  24970  log2sumbnd  24978  selberglem1  24979  selberglem2  24980  selberg2lem  24984  selberg2  24985  pntrmax  24998  pntrsumo1  24999  selbergr  25002  pntlem3  25043  pnt2  25047  xrge0iifhom  29105  omssubadd  29483  signsplypnf  29747  signsply0  29748  taupilem2  32139  taupi  32140  ptrecube  32373  heicant  32408  totbndbnd  32552  rpexpmord  36325  seff  37324  ioorrnopnlem  38994  vonioolem1  39365  elbigolo1  42141  amgmwlem  42310  amgmlemALT  42311
  Copyright terms: Public domain W3C validator