Step |
Hyp |
Ref |
Expression |
1 |
|
logdivlt |
|- ( ( ( B e. RR /\ _e <_ B ) /\ ( A e. RR /\ _e <_ A ) ) -> ( B < A <-> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) ) |
2 |
1
|
ancoms |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( B < A <-> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) ) |
3 |
2
|
notbid |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( -. B < A <-> -. ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) ) |
4 |
|
simpll |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> A e. RR ) |
5 |
|
simprl |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> B e. RR ) |
6 |
4 5
|
lenltd |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A <_ B <-> -. B < A ) ) |
7 |
|
0red |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> 0 e. RR ) |
8 |
|
ere |
|- _e e. RR |
9 |
8
|
a1i |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> _e e. RR ) |
10 |
|
epos |
|- 0 < _e |
11 |
10
|
a1i |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> 0 < _e ) |
12 |
|
simprr |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> _e <_ B ) |
13 |
7 9 5 11 12
|
ltletrd |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> 0 < B ) |
14 |
5 13
|
elrpd |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> B e. RR+ ) |
15 |
|
relogcl |
|- ( B e. RR+ -> ( log ` B ) e. RR ) |
16 |
14 15
|
syl |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( log ` B ) e. RR ) |
17 |
16 14
|
rerpdivcld |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( ( log ` B ) / B ) e. RR ) |
18 |
|
simplr |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> _e <_ A ) |
19 |
7 9 4 11 18
|
ltletrd |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> 0 < A ) |
20 |
4 19
|
elrpd |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> A e. RR+ ) |
21 |
|
relogcl |
|- ( A e. RR+ -> ( log ` A ) e. RR ) |
22 |
20 21
|
syl |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( log ` A ) e. RR ) |
23 |
22 20
|
rerpdivcld |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( ( log ` A ) / A ) e. RR ) |
24 |
17 23
|
lenltd |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( ( ( log ` B ) / B ) <_ ( ( log ` A ) / A ) <-> -. ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) ) |
25 |
3 6 24
|
3bitr4d |
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A <_ B <-> ( ( log ` B ) / B ) <_ ( ( log ` A ) / A ) ) ) |