![]() |
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 12138 | . 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | 1 | ssrab3 3909 | 1 ⊢ ℝ+ ⊆ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3792 class class class wbr 4886 ℝcr 10271 0cc0 10272 < clt 10411 ℝ+crp 12137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-in 3799 df-ss 3806 df-rp 12138 |
This theorem is referenced by: rpre 12145 rpred 12181 rpexpcl 13197 sqrlem3 14392 fsumrpcl 14875 o1fsum 14949 divrcnv 14988 fprodrpcl 15089 rprisefaccl 15156 lebnumlem2 23169 bcthlem1 23530 bcthlem5 23534 aalioulem2 24525 efcvx 24640 pilem2 24643 pilem3 24644 pilem3OLD 24645 dvrelog 24820 relogcn 24821 logcn 24830 advlog 24837 advlogexp 24838 loglesqrt 24939 rlimcnp 25144 rlimcnp3 25146 cxplim 25150 cxp2lim 25155 cxploglim 25156 divsqrtsumo1 25162 amgmlem 25168 logexprlim 25402 chto1ub 25617 chpo1ub 25621 chpo1ubb 25622 vmadivsum 25623 vmadivsumb 25624 rpvmasumlem 25628 dchrmusum2 25635 dchrvmasumlem2 25639 dchrvmasumiflem2 25643 dchrisum0fno1 25652 rpvmasum2 25653 dchrisum0lem1 25657 dchrisum0lem2a 25658 dchrisum0lem2 25659 dchrisum0 25661 dchrmusumlem 25663 rplogsum 25668 dirith2 25669 mudivsum 25671 mulogsumlem 25672 mulogsum 25673 mulog2sumlem2 25676 mulog2sumlem3 25677 log2sumbnd 25685 selberglem1 25686 selberglem2 25687 selberg2lem 25691 selberg2 25692 pntrmax 25705 pntrsumo1 25706 selbergr 25709 pntlem3 25750 pnt2 25754 rpdp2cl 30152 dp2lt10 30154 dp2lt 30155 dp2ltc 30157 xrge0iifhom 30581 omssubadd 30960 signsplypnf 31227 signsply0 31228 rpsqrtcn 31273 taupilem2 33764 taupi 33765 ptrecube 34035 heicant 34070 totbndbnd 34212 rpexpmord 38472 seff 39464 rpssxr 40616 ioorrnopnlem 41448 vonioolem1 41821 elbigolo1 43366 amgmwlem 43654 amgmlemALT 43655 |
Copyright terms: Public domain | W3C validator |