Step |
Hyp |
Ref |
Expression |
1 |
|
cxplt |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( C e. RR /\ B e. RR ) ) -> ( C < B <-> ( A ^c C ) < ( A ^c B ) ) ) |
2 |
1
|
ancom2s |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( C < B <-> ( A ^c C ) < ( A ^c B ) ) ) |
3 |
2
|
notbid |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( -. C < B <-> -. ( A ^c C ) < ( A ^c B ) ) ) |
4 |
|
lenlt |
|- ( ( B e. RR /\ C e. RR ) -> ( B <_ C <-> -. C < B ) ) |
5 |
4
|
adantl |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> -. C < B ) ) |
6 |
|
simpll |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> A e. RR ) |
7 |
|
0red |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 e. RR ) |
8 |
|
1red |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 1 e. RR ) |
9 |
|
0lt1 |
|- 0 < 1 |
10 |
9
|
a1i |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 < 1 ) |
11 |
|
simplr |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 1 < A ) |
12 |
7 8 6 10 11
|
lttrd |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 < A ) |
13 |
7 6 12
|
ltled |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 <_ A ) |
14 |
|
simprl |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> B e. RR ) |
15 |
|
recxpcl |
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR ) |
16 |
6 13 14 15
|
syl3anc |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c B ) e. RR ) |
17 |
|
simprr |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> C e. RR ) |
18 |
|
recxpcl |
|- ( ( A e. RR /\ 0 <_ A /\ C e. RR ) -> ( A ^c C ) e. RR ) |
19 |
6 13 17 18
|
syl3anc |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c C ) e. RR ) |
20 |
16 19
|
lenltd |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( A ^c B ) <_ ( A ^c C ) <-> -. ( A ^c C ) < ( A ^c B ) ) ) |
21 |
3 5 20
|
3bitr4d |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> ( A ^c B ) <_ ( A ^c C ) ) ) |