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 9442 | . . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | ssrab2 3182 | . . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ | |
3 | 1, 2 | eqsstri 3129 | . 2 ⊢ ℝ+ ⊆ ℝ |
4 | 3 | sseli 3093 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 {crab 2420 class class class wbr 3929 ℝcr 7619 0cc0 7620 < clt 7800 ℝ+crp 9441 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rab 2425 df-in 3077 df-ss 3084 df-rp 9442 |
This theorem is referenced by: rpxr 9449 rpcn 9450 rpssre 9452 rpge0 9454 rprege0 9456 rpap0 9458 rprene0 9459 rpreap0 9460 rpaddcl 9465 rpmulcl 9466 rpdivcl 9467 rpgecl 9470 ledivge1le 9513 addlelt 9555 iccdil 9781 expnlbnd 10416 caucvgre 10753 rennim 10774 rpsqrtcl 10813 qdenre 10974 rpmaxcl 10995 rpmincl 11009 xrminrpcl 11043 2clim 11070 cn1lem 11083 climsqz 11104 climsqz2 11105 climcau 11116 efgt1 11403 ef01bndlem 11463 bdmet 12671 bdmopn 12673 dveflem 12855 |
Copyright terms: Public domain | W3C validator |