Theorem rpssre 11719

Description: The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)

Assertion

Ref	Expression
rpssre	⊢ ℝ+ ⊆ ℝ

Proof of Theorem rpssre

Step	Hyp	Ref	Expression
1		rpre 11715	. 2 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
2	1	ssriv 3572	1 ⊢ ℝ+ ⊆ ℝ

Syntax hints:   ⊆ wss 3540  ℝcr 9814  ℝ⁺crp 11708

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 11709

This theorem is referenced by:  rpred  11748  rpexpcl  12741  sqrlem3  13833  fsumrpcl  14315  o1fsum  14386  divrcnv  14423  fprodrpcl  14525  rprisefaccl  14593  lebnumlem2  22569  bcthlem1  22929  bcthlem5  22933  aalioulem2  23892  efcvx  24007  pilem2  24010  pilem3  24011  dvrelog  24183  relogcn  24184  logcn  24193  advlog  24200  advlogexp  24201  loglesqrt  24299  rlimcnp  24492  rlimcnp3  24494  cxplim  24498  cxp2lim  24503  cxploglim  24504  divsqrtsumo1  24510  amgmlem  24516  logexprlim  24750  chto1ub  24965  chpo1ub  24969  chpo1ubb  24970  vmadivsum  24971  vmadivsumb  24972  rpvmasumlem  24976  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumiflem2  24991  dchrisum0fno1  25000  rpvmasum2  25001  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0  25009  dchrmusumlem  25011  rplogsum  25016  dirith2  25017  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  mulog2sumlem2  25024  mulog2sumlem3  25025  log2sumbnd  25033  selberglem1  25034  selberglem2  25035  selberg2lem  25039  selberg2  25040  pntrmax  25053  pntrsumo1  25054  selbergr  25057  pntlem3  25098  pnt2  25102  xrge0iifhom  29311  omssubadd  29689  signsplypnf  29953  signsply0  29954  taupilem2  32345  taupi  32346  ptrecube  32579  heicant  32614  totbndbnd  32758  rpexpmord  36531  seff  37530  ioorrnopnlem  39200  vonioolem1  39571  elbigolo1  42149  amgmwlem  42357  amgmlemALT  42358