![]() |
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 9642 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | sylanbrc 417 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rab 2464 df-v 2739 df-un 3133 df-sn 3597 df-pr 3598 df-op 3600 df-br 4001 df-rp 9641 |
This theorem is referenced by: mul2lt0rgt0 9747 mul2lt0np 9750 zltaddlt1le 9994 modqval 10310 ltexp2a 10558 leexp2a 10559 expnlbnd2 10631 nn0ltexp2 10674 resqrexlem1arp 10998 resqrexlemp1rp 10999 resqrexlemcalc2 11008 resqrexlemcalc3 11009 resqrexlemgt0 11013 resqrexlemglsq 11015 rpsqrtcl 11034 absrpclap 11054 rpmaxcl 11216 rpmincl 11230 xrminrpcl 11266 xrbdtri 11268 mulcn2 11304 reccn2ap 11305 climge0 11317 divcnv 11489 georeclim 11505 cvgratnnlembern 11515 cvgratnnlemsumlt 11520 cvgratnnlemfm 11521 cvgratnnlemrate 11522 cvgratnn 11523 cvgratz 11524 rpefcl 11677 efltim 11690 ef01bndlem 11748 pythagtriplem12 12258 pythagtriplem14 12260 pythagtriplem16 12262 bdmopn 13671 mulcncflem 13757 ivthinclemlopn 13781 ivthinclemuopn 13783 dveflem 13854 reeff1olem 13859 pilem3 13871 tanrpcl 13925 cosordlem 13937 rplogcl 13967 logdivlti 13969 cxplt 14003 cxple 14004 rpabscxpbnd 14026 ltexp2 14027 iooref1o 14438 |
Copyright terms: Public domain | W3C validator |