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

Theorem rpssre 11881
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 11877 . 2 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
21ssriv 3640 1 + ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3607  cr 9973  +crp 11870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-in 3614  df-ss 3621  df-rp 11871
This theorem is referenced by:  rpred  11910  rpexpcl  12919  sqrlem3  14029  fsumrpcl  14512  o1fsum  14589  divrcnv  14628  fprodrpcl  14730  rprisefaccl  14798  lebnumlem2  22808  bcthlem1  23167  bcthlem5  23171  aalioulem2  24133  efcvx  24248  pilem2  24251  pilem3  24252  dvrelog  24428  relogcn  24429  logcn  24438  advlog  24445  advlogexp  24446  loglesqrt  24544  rlimcnp  24737  rlimcnp3  24739  cxplim  24743  cxp2lim  24748  cxploglim  24749  divsqrtsumo1  24755  amgmlem  24761  logexprlim  24995  chto1ub  25210  chpo1ub  25214  chpo1ubb  25215  vmadivsum  25216  vmadivsumb  25217  rpvmasumlem  25221  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumiflem2  25236  dchrisum0fno1  25245  rpvmasum2  25246  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0  25254  dchrmusumlem  25256  rplogsum  25261  dirith2  25262  mudivsum  25264  mulogsumlem  25265  mulogsum  25266  mulog2sumlem2  25269  mulog2sumlem3  25270  log2sumbnd  25278  selberglem1  25279  selberglem2  25280  selberg2lem  25284  selberg2  25285  pntrmax  25298  pntrsumo1  25299  selbergr  25302  pntlem3  25343  pnt2  25347  rpdp2cl  29717  dp2lt10  29719  dp2lt  29720  dp2ltc  29722  xrge0iifhom  30111  omssubadd  30490  signsplypnf  30755  signsply0  30756  rpsqrtcn  30799  taupilem2  33298  taupi  33299  ptrecube  33539  heicant  33574  totbndbnd  33718  rpexpmord  37830  seff  38825  rpssxr  40024  ioorrnopnlem  40842  vonioolem1  41215  elbigolo1  42676  amgmwlem  42876  amgmlemALT  42877
  Copyright terms: Public domain W3C validator