Metamath Proof Explorer

Theorem logdivle

Description: The log x / x function is strictly decreasing on the reals greater than _e . (Contributed by Mario Carneiro, 3-May-2016)

Ref Expression
Assertion logdivle 
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A <_ B <-> ( ( log ` B ) / B ) <_ ( ( log ` A ) / A ) ) )

Proof

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 ) ) )