Step |
Hyp |
Ref |
Expression |
1 |
|
cxplt3 |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( C e. RR /\ B e. RR ) ) -> ( C < B <-> ( A ^c B ) < ( A ^c C ) ) ) |
2 |
1
|
ancom2s |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( C < B <-> ( A ^c B ) < ( A ^c C ) ) ) |
3 |
2
|
notbid |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( -. C < B <-> -. ( A ^c B ) < ( A ^c C ) ) ) |
4 |
|
lenlt |
|- ( ( B e. RR /\ C e. RR ) -> ( B <_ C <-> -. C < B ) ) |
5 |
4
|
adantl |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> -. C < B ) ) |
6 |
|
rpcxpcl |
|- ( ( A e. RR+ /\ C e. RR ) -> ( A ^c C ) e. RR+ ) |
7 |
6
|
ad2ant2rl |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c C ) e. RR+ ) |
8 |
|
rpcxpcl |
|- ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR+ ) |
9 |
8
|
ad2ant2r |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c B ) e. RR+ ) |
10 |
|
rpre |
|- ( ( A ^c C ) e. RR+ -> ( A ^c C ) e. RR ) |
11 |
|
rpre |
|- ( ( A ^c B ) e. RR+ -> ( A ^c B ) e. RR ) |
12 |
|
lenlt |
|- ( ( ( A ^c C ) e. RR /\ ( A ^c B ) e. RR ) -> ( ( A ^c C ) <_ ( A ^c B ) <-> -. ( A ^c B ) < ( A ^c C ) ) ) |
13 |
10 11 12
|
syl2an |
|- ( ( ( A ^c C ) e. RR+ /\ ( A ^c B ) e. RR+ ) -> ( ( A ^c C ) <_ ( A ^c B ) <-> -. ( A ^c B ) < ( A ^c C ) ) ) |
14 |
7 9 13
|
syl2anc |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( A ^c C ) <_ ( A ^c B ) <-> -. ( A ^c B ) < ( A ^c C ) ) ) |
15 |
3 5 14
|
3bitr4d |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> ( A ^c C ) <_ ( A ^c B ) ) ) |