![]() |
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 9189 | . . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | ssrab2 3107 | . . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ | |
3 | 1, 2 | eqsstri 3057 | . 2 ⊢ ℝ+ ⊆ ℝ |
4 | 3 | sseli 3022 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1439 {crab 2364 class class class wbr 3851 ℝcr 7403 0cc0 7404 < clt 7576 ℝ+crp 9188 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-rab 2369 df-in 3006 df-ss 3013 df-rp 9189 |
This theorem is referenced by: rpxr 9195 rpcn 9196 rpssre 9198 rpge0 9200 rprege0 9202 rpap0 9204 rprene0 9205 rpreap0 9206 rpaddcl 9211 rpmulcl 9212 rpdivcl 9213 rpgecl 9216 ledivge1le 9257 addlelt 9293 iccdil 9469 expnlbnd 10132 caucvgre 10468 rennim 10489 rpsqrtcl 10528 qdenre 10689 2clim 10743 cn1lem 10756 climsqz 10777 climsqz2 10778 climcau 10790 efgt1 11041 ef01bndlem 11101 |
Copyright terms: Public domain | W3C validator |