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 12731 | . 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | 1 | ssrab3 4015 | 1 ⊢ ℝ+ ⊆ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3887 class class class wbr 5074 ℝcr 10870 0cc0 10871 < clt 11009 ℝ+crp 12730 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-in 3894 df-ss 3904 df-rp 12731 |
This theorem is referenced by: rpre 12738 rpred 12772 rpexpcl 13801 rpexpmord 13886 sqrlem3 14956 fsumrpcl 15449 o1fsum 15525 divrcnv 15564 fprodrpcl 15666 rprisefaccl 15733 lebnumlem2 24125 bcthlem1 24488 bcthlem5 24492 aalioulem2 25493 efcvx 25608 pilem2 25611 pilem3 25612 dvrelog 25792 relogcn 25793 logcn 25802 advlog 25809 advlogexp 25810 loglesqrt 25911 rlimcnp 26115 rlimcnp3 26117 cxplim 26121 cxp2lim 26126 cxploglim 26127 divsqrtsumo1 26133 amgmlem 26139 logexprlim 26373 chto1ub 26624 chpo1ub 26628 chpo1ubb 26629 vmadivsum 26630 vmadivsumb 26631 rpvmasumlem 26635 dchrmusum2 26642 dchrvmasumlem2 26646 dchrvmasumiflem2 26650 dchrisum0fno1 26659 rpvmasum2 26660 dchrisum0lem1 26664 dchrisum0lem2a 26665 dchrisum0lem2 26666 dchrisum0 26668 dchrmusumlem 26670 rplogsum 26675 dirith2 26676 mudivsum 26678 mulogsumlem 26679 mulogsum 26680 mulog2sumlem2 26683 mulog2sumlem3 26684 log2sumbnd 26692 selberglem1 26693 selberglem2 26694 selberg2lem 26698 selberg2 26699 pntrmax 26712 pntrsumo1 26713 selbergr 26716 pntlem3 26757 pnt2 26761 rpdp2cl 31156 dp2lt10 31158 dp2lt 31159 dp2ltc 31161 xrge0iifhom 31887 omssubadd 32267 signsplypnf 32529 signsply0 32530 rpsqrtcn 32573 taupilem2 35493 taupi 35494 ptrecube 35777 heicant 35812 totbndbnd 35947 dvrelog2 40072 dvrelog3 40073 seff 41927 rpssxr 43021 ioorrnopnlem 43845 vonioolem1 44218 elbigolo1 45903 amgmwlem 46506 amgmlemALT 46507 |
Copyright terms: Public domain | W3C validator |