Step |
Hyp |
Ref |
Expression |
1 |
|
simprl |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> B e. RR ) |
2 |
|
rplogcl |
|- ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ ) |
3 |
2
|
adantr |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( log ` A ) e. RR+ ) |
4 |
3
|
rpred |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( log ` A ) e. RR ) |
5 |
1 4
|
remulcld |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B x. ( log ` A ) ) e. RR ) |
6 |
|
simprr |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> C e. RR ) |
7 |
6 4
|
remulcld |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( C x. ( log ` A ) ) e. RR ) |
8 |
|
eflt |
|- ( ( ( B x. ( log ` A ) ) e. RR /\ ( C x. ( log ` A ) ) e. RR ) -> ( ( B x. ( log ` A ) ) < ( C x. ( log ` A ) ) <-> ( exp ` ( B x. ( log ` A ) ) ) < ( exp ` ( C x. ( log ` A ) ) ) ) ) |
9 |
5 7 8
|
syl2anc |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( B x. ( log ` A ) ) < ( C x. ( log ` A ) ) <-> ( exp ` ( B x. ( log ` A ) ) ) < ( exp ` ( C x. ( log ` A ) ) ) ) ) |
10 |
1 6 3
|
ltmul1d |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B < C <-> ( B x. ( log ` A ) ) < ( C x. ( log ` A ) ) ) ) |
11 |
|
simpll |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> A e. RR ) |
12 |
11
|
recnd |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> A e. CC ) |
13 |
|
0red |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 e. RR ) |
14 |
|
1red |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 1 e. RR ) |
15 |
|
0lt1 |
|- 0 < 1 |
16 |
15
|
a1i |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 < 1 ) |
17 |
|
simplr |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 1 < A ) |
18 |
13 14 11 16 17
|
lttrd |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 < A ) |
19 |
18
|
gt0ne0d |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> A =/= 0 ) |
20 |
1
|
recnd |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> B e. CC ) |
21 |
|
cxpef |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) ) |
22 |
12 19 20 21
|
syl3anc |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) ) |
23 |
6
|
recnd |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> C e. CC ) |
24 |
|
cxpef |
|- ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) ) |
25 |
12 19 23 24
|
syl3anc |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) ) |
26 |
22 25
|
breq12d |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( A ^c B ) < ( A ^c C ) <-> ( exp ` ( B x. ( log ` A ) ) ) < ( exp ` ( C x. ( log ` A ) ) ) ) ) |
27 |
9 10 26
|
3bitr4d |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B < C <-> ( A ^c B ) < ( A ^c C ) ) ) |