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

Theorem rpssre 12388
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 df-rp 12382 . 2 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
21ssrab3 4055 1 + ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3934   class class class wbr 5057  cr 10528  0cc0 10529   < clt 10667  +crp 12381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-in 3941  df-ss 3950  df-rp 12382
This theorem is referenced by:  rpre  12389  rpred  12423  rpexpcl  13440  rpexpmord  13524  sqrlem3  14596  fsumrpcl  15086  o1fsum  15160  divrcnv  15199  fprodrpcl  15302  rprisefaccl  15369  lebnumlem2  23558  bcthlem1  23919  bcthlem5  23923  aalioulem2  24914  efcvx  25029  pilem2  25032  pilem3  25033  dvrelog  25212  relogcn  25213  logcn  25222  advlog  25229  advlogexp  25230  loglesqrt  25331  rlimcnp  25535  rlimcnp3  25537  cxplim  25541  cxp2lim  25546  cxploglim  25547  divsqrtsumo1  25553  amgmlem  25559  logexprlim  25793  chto1ub  26044  chpo1ub  26048  chpo1ubb  26049  vmadivsum  26050  vmadivsumb  26051  rpvmasumlem  26055  dchrmusum2  26062  dchrvmasumlem2  26066  dchrvmasumiflem2  26070  dchrisum0fno1  26079  rpvmasum2  26080  dchrisum0lem1  26084  dchrisum0lem2a  26085  dchrisum0lem2  26086  dchrisum0  26088  dchrmusumlem  26090  rplogsum  26095  dirith2  26096  mudivsum  26098  mulogsumlem  26099  mulogsum  26100  mulog2sumlem2  26103  mulog2sumlem3  26104  log2sumbnd  26112  selberglem1  26113  selberglem2  26114  selberg2lem  26118  selberg2  26119  pntrmax  26132  pntrsumo1  26133  selbergr  26136  pntlem3  26177  pnt2  26181  rpdp2cl  30551  dp2lt10  30553  dp2lt  30554  dp2ltc  30556  xrge0iifhom  31173  omssubadd  31551  signsplypnf  31813  signsply0  31814  rpsqrtcn  31857  taupilem2  34595  taupi  34596  ptrecube  34884  heicant  34919  totbndbnd  35059  seff  40631  rpssxr  41746  ioorrnopnlem  42579  vonioolem1  42952  elbigolo1  44607  amgmwlem  44893  amgmlemALT  44894
  Copyright terms: Public domain W3C validator