Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rpre | GIF version |
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
rpre | ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rp 9611 | . . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | ssrab2 3232 | . . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ | |
3 | 1, 2 | eqsstri 3179 | . 2 ⊢ ℝ+ ⊆ ℝ |
4 | 3 | sseli 3143 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 {crab 2452 class class class wbr 3989 ℝcr 7773 0cc0 7774 < clt 7954 ℝ+crp 9610 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-rab 2457 df-in 3127 df-ss 3134 df-rp 9611 |
This theorem is referenced by: rpxr 9618 rpcn 9619 rpssre 9621 rpge0 9623 rprege0 9625 rpap0 9627 rprene0 9628 rpreap0 9629 rpaddcl 9634 rpmulcl 9635 rpdivcl 9636 rpgecl 9639 ledivge1le 9683 addlelt 9725 iccdil 9955 expnlbnd 10600 caucvgre 10945 rennim 10966 rpsqrtcl 11005 qdenre 11166 rpmaxcl 11187 rpmincl 11201 xrminrpcl 11237 2clim 11264 cn1lem 11277 climsqz 11298 climsqz2 11299 climcau 11310 efgt1 11660 ef01bndlem 11719 bdmet 13296 bdmopn 13298 dveflem 13481 reeff1o 13488 logleb 13590 logrpap0b 13591 cxple3 13635 rpcxpsqrt 13636 rpcxpsqrtth 13644 dceqnconst 14091 dcapnconst 14092 |
Copyright terms: Public domain | W3C validator |