Step |
Hyp |
Ref |
Expression |
1 |
|
simpll |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> A e. RR+ ) |
2 |
|
simprl |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> B e. RR ) |
3 |
2
|
recnd |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> B e. CC ) |
4 |
|
cxprec |
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) ) |
5 |
1 3 4
|
syl2anc |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) ) |
6 |
|
simprr |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> C e. RR ) |
7 |
6
|
recnd |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> C e. CC ) |
8 |
|
cxprec |
|- ( ( A e. RR+ /\ C e. CC ) -> ( ( 1 / A ) ^c C ) = ( 1 / ( A ^c C ) ) ) |
9 |
1 7 8
|
syl2anc |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( 1 / A ) ^c C ) = ( 1 / ( A ^c C ) ) ) |
10 |
5 9
|
breq12d |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( ( 1 / A ) ^c B ) < ( ( 1 / A ) ^c C ) <-> ( 1 / ( A ^c B ) ) < ( 1 / ( A ^c C ) ) ) ) |
11 |
1
|
rprecred |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( 1 / A ) e. RR ) |
12 |
|
simplr |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> A < 1 ) |
13 |
1
|
reclt1d |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( A < 1 <-> 1 < ( 1 / A ) ) ) |
14 |
12 13
|
mpbid |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> 1 < ( 1 / A ) ) |
15 |
|
cxplt |
|- ( ( ( ( 1 / A ) e. RR /\ 1 < ( 1 / A ) ) /\ ( B e. RR /\ C e. RR ) ) -> ( B < C <-> ( ( 1 / A ) ^c B ) < ( ( 1 / A ) ^c C ) ) ) |
16 |
11 14 2 6 15
|
syl22anc |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B < C <-> ( ( 1 / A ) ^c B ) < ( ( 1 / A ) ^c C ) ) ) |
17 |
|
rpcxpcl |
|- ( ( A e. RR+ /\ C e. RR ) -> ( A ^c C ) e. RR+ ) |
18 |
17
|
ad2ant2rl |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c C ) e. RR+ ) |
19 |
|
rpcxpcl |
|- ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR+ ) |
20 |
19
|
ad2ant2r |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c B ) e. RR+ ) |
21 |
18 20
|
ltrecd |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( A ^c C ) < ( A ^c B ) <-> ( 1 / ( A ^c B ) ) < ( 1 / ( A ^c C ) ) ) ) |
22 |
10 16 21
|
3bitr4d |
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B < C <-> ( A ^c C ) < ( A ^c B ) ) ) |