![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rpre | Unicode version |
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
rpre |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rp 9234 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssrab2 3121 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqsstri 3071 |
. 2
![]() ![]() ![]() ![]() |
4 | 3 | sseli 3035 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-rab 2379 df-in 3019 df-ss 3026 df-rp 9234 |
This theorem is referenced by: rpxr 9240 rpcn 9241 rpssre 9243 rpge0 9245 rprege0 9247 rpap0 9249 rprene0 9250 rpreap0 9251 rpaddcl 9256 rpmulcl 9257 rpdivcl 9258 rpgecl 9261 ledivge1le 9302 addlelt 9338 iccdil 9564 expnlbnd 10193 caucvgre 10529 rennim 10550 rpsqrtcl 10589 qdenre 10750 rpmincl 10784 xrminrpcl 10817 2clim 10844 cn1lem 10857 climsqz 10878 climsqz2 10879 climcau 10890 efgt1 11136 ef01bndlem 11196 bdmet 12288 bdmopn 12290 |
Copyright terms: Public domain | W3C validator |