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

Theorem rpssre 12056
 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 12052 . 2 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
21ssriv 3748 1 + ⊆ ℝ
 Colors of variables: wff setvar class Syntax hints:   ⊆ wss 3715  ℝcr 10147  ℝ+crp 12045 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-in 3722  df-ss 3729  df-rp 12046 This theorem is referenced by:  rpred  12085  rpexpcl  13093  sqrlem3  14204  fsumrpcl  14687  o1fsum  14764  divrcnv  14803  fprodrpcl  14905  rprisefaccl  14973  lebnumlem2  22982  bcthlem1  23341  bcthlem5  23345  aalioulem2  24307  efcvx  24422  pilem2  24425  pilem3  24426  pilem3OLD  24427  dvrelog  24603  relogcn  24604  logcn  24613  advlog  24620  advlogexp  24621  loglesqrt  24719  rlimcnp  24912  rlimcnp3  24914  cxplim  24918  cxp2lim  24923  cxploglim  24924  divsqrtsumo1  24930  amgmlem  24936  logexprlim  25170  chto1ub  25385  chpo1ub  25389  chpo1ubb  25390  vmadivsum  25391  vmadivsumb  25392  rpvmasumlem  25396  dchrmusum2  25403  dchrvmasumlem2  25407  dchrvmasumiflem2  25411  dchrisum0fno1  25420  rpvmasum2  25421  dchrisum0lem1  25425  dchrisum0lem2a  25426  dchrisum0lem2  25427  dchrisum0  25429  dchrmusumlem  25431  rplogsum  25436  dirith2  25437  mudivsum  25439  mulogsumlem  25440  mulogsum  25441  mulog2sumlem2  25444  mulog2sumlem3  25445  log2sumbnd  25453  selberglem1  25454  selberglem2  25455  selberg2lem  25459  selberg2  25460  pntrmax  25473  pntrsumo1  25474  selbergr  25477  pntlem3  25518  pnt2  25522  rpdp2cl  29919  dp2lt10  29921  dp2lt  29922  dp2ltc  29924  xrge0iifhom  30313  omssubadd  30692  signsplypnf  30957  signsply0  30958  rpsqrtcn  31001  taupilem2  33497  taupi  33498  ptrecube  33740  heicant  33775  totbndbnd  33919  rpexpmord  38033  seff  39028  rpssxr  40227  ioorrnopnlem  41045  vonioolem1  41418  elbigolo1  42879  amgmwlem  43079  amgmlemALT  43080
 Copyright terms: Public domain W3C validator