![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpssre | Structured version Visualization version GIF version |
Description: The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.) |
Ref | Expression |
---|---|
rpssre | ⊢ ℝ+ ⊆ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rp 12971 | . 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | 1 | ssrab3 4072 | 1 ⊢ ℝ+ ⊆ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3940 class class class wbr 5138 ℝcr 11104 0cc0 11105 < clt 11244 ℝ+crp 12970 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rab 3425 df-v 3468 df-in 3947 df-ss 3957 df-rp 12971 |
This theorem is referenced by: rpre 12978 rpred 13012 rpexpcl 14042 rpexpmord 14129 01sqrexlem3 15187 fsumrpcl 15679 o1fsum 15755 divrcnv 15794 fprodrpcl 15896 rprisefaccl 15963 lebnumlem2 24798 bcthlem1 25162 bcthlem5 25166 aalioulem2 26175 efcvx 26291 pilem2 26294 pilem3 26295 dvrelog 26475 relogcn 26476 logcn 26485 advlog 26492 advlogexp 26493 loglesqrt 26597 rlimcnp 26801 rlimcnp3 26803 cxplim 26808 cxp2lim 26813 cxploglim 26814 divsqrtsumo1 26820 amgmlem 26826 logexprlim 27062 chto1ub 27313 chpo1ub 27317 chpo1ubb 27318 vmadivsum 27319 vmadivsumb 27320 rpvmasumlem 27324 dchrmusum2 27331 dchrvmasumlem2 27335 dchrvmasumiflem2 27339 dchrisum0fno1 27348 rpvmasum2 27349 dchrisum0lem1 27353 dchrisum0lem2a 27354 dchrisum0lem2 27355 dchrisum0 27357 dchrmusumlem 27359 rplogsum 27364 dirith2 27365 mudivsum 27367 mulogsumlem 27368 mulogsum 27369 mulog2sumlem2 27372 mulog2sumlem3 27373 log2sumbnd 27381 selberglem1 27382 selberglem2 27383 selberg2lem 27387 selberg2 27388 pntrmax 27401 pntrsumo1 27402 selbergr 27405 pntlem3 27446 pnt2 27450 rpdp2cl 32472 dp2lt10 32474 dp2lt 32475 dp2ltc 32477 xrge0iifhom 33372 omssubadd 33754 signsplypnf 34016 signsply0 34017 rpsqrtcn 34060 taupilem2 36659 taupi 36660 ptrecube 36944 heicant 36979 totbndbnd 37113 dvrelog2 41388 dvrelog3 41389 seff 43523 rpssxr 44642 ioorrnopnlem 45471 vonioolem1 45847 elbigolo1 47397 amgmwlem 48003 amgmlemALT 48004 |
Copyright terms: Public domain | W3C validator |