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 12485 | . 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | 1 | ssrab3 3981 | 1 ⊢ ℝ+ ⊆ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3853 class class class wbr 5040 ℝcr 10626 0cc0 10627 < clt 10765 ℝ+crp 12484 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-rab 3063 df-v 3402 df-in 3860 df-ss 3870 df-rp 12485 |
This theorem is referenced by: rpre 12492 rpred 12526 rpexpcl 13552 rpexpmord 13636 sqrlem3 14706 fsumrpcl 15199 o1fsum 15273 divrcnv 15312 fprodrpcl 15414 rprisefaccl 15481 lebnumlem2 23726 bcthlem1 24088 bcthlem5 24092 aalioulem2 25093 efcvx 25208 pilem2 25211 pilem3 25212 dvrelog 25392 relogcn 25393 logcn 25402 advlog 25409 advlogexp 25410 loglesqrt 25511 rlimcnp 25715 rlimcnp3 25717 cxplim 25721 cxp2lim 25726 cxploglim 25727 divsqrtsumo1 25733 amgmlem 25739 logexprlim 25973 chto1ub 26224 chpo1ub 26228 chpo1ubb 26229 vmadivsum 26230 vmadivsumb 26231 rpvmasumlem 26235 dchrmusum2 26242 dchrvmasumlem2 26246 dchrvmasumiflem2 26250 dchrisum0fno1 26259 rpvmasum2 26260 dchrisum0lem1 26264 dchrisum0lem2a 26265 dchrisum0lem2 26266 dchrisum0 26268 dchrmusumlem 26270 rplogsum 26275 dirith2 26276 mudivsum 26278 mulogsumlem 26279 mulogsum 26280 mulog2sumlem2 26283 mulog2sumlem3 26284 log2sumbnd 26292 selberglem1 26293 selberglem2 26294 selberg2lem 26298 selberg2 26299 pntrmax 26312 pntrsumo1 26313 selbergr 26316 pntlem3 26357 pnt2 26361 rpdp2cl 30743 dp2lt10 30745 dp2lt 30746 dp2ltc 30748 xrge0iifhom 31471 omssubadd 31849 signsplypnf 32111 signsply0 32112 rpsqrtcn 32155 taupilem2 35145 taupi 35146 ptrecube 35432 heicant 35467 totbndbnd 35602 dvrelog2 39723 dvrelog3 39724 seff 41505 rpssxr 42601 ioorrnopnlem 43427 vonioolem1 43800 elbigolo1 45484 amgmwlem 46006 amgmlemALT 46007 |
Copyright terms: Public domain | W3C validator |