Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elrpd | Unicode version |
Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
elrpd.1 | |
elrpd.2 |
Ref | Expression |
---|---|
elrpd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrpd.1 | . 2 | |
2 | elrpd.2 | . 2 | |
3 | elrp 9443 | . 2 | |
4 | 1, 2, 3 | sylanbrc 413 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 class class class wbr 3929 cr 7619 cc0 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-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rab 2425 df-v 2688 df-un 3075 df-sn 3533 df-pr 3534 df-op 3536 df-br 3930 df-rp 9442 |
This theorem is referenced by: mul2lt0rgt0 9547 mul2lt0np 9550 zltaddlt1le 9789 modqval 10097 ltexp2a 10345 leexp2a 10346 expnlbnd2 10417 resqrexlem1arp 10777 resqrexlemp1rp 10778 resqrexlemcalc2 10787 resqrexlemcalc3 10788 resqrexlemgt0 10792 resqrexlemglsq 10794 rpsqrtcl 10813 absrpclap 10833 rpmaxcl 10995 rpmincl 11009 xrminrpcl 11043 xrbdtri 11045 mulcn2 11081 reccn2ap 11082 climge0 11094 divcnv 11266 georeclim 11282 cvgratnnlembern 11292 cvgratnnlemsumlt 11297 cvgratnnlemfm 11298 cvgratnnlemrate 11299 cvgratnn 11300 cvgratz 11301 rpefcl 11391 efltim 11404 ef01bndlem 11463 bdmopn 12673 mulcncflem 12759 ivthinclemlopn 12783 ivthinclemuopn 12785 dveflem 12855 pilem3 12864 tanrpcl 12918 cosordlem 12930 |
Copyright terms: Public domain | W3C validator |