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