Metamath Proof Explorer

Theorem logdivlt

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

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

Proof

Step Hyp Ref Expression
1 logdivlti 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) )
2 1 ex 
 |-  ( ( A e. RR /\ B e. RR /\ _e <_ A ) -> ( A < B -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) ) )
3 2 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ _e <_ A ) -> ( A < B -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) ) )
4 3 an32s 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ B e. RR ) -> ( A < B -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) ) )
5 4 adantrr 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A < B -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) ) )
6 fveq2 
 |-  ( A = B -> ( log ` A ) = ( log ` B ) )
7 id 
 |-  ( A = B -> A = B )
8 6 7 oveq12d 
 |-  ( A = B -> ( ( log ` A ) / A ) = ( ( log ` B ) / B ) )
9 8 eqcomd 
 |-  ( A = B -> ( ( log ` B ) / B ) = ( ( log ` A ) / A ) )
10 9 a1i 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A = B -> ( ( log ` B ) / B ) = ( ( log ` A ) / A ) ) )
11 logdivlti 
 |-  ( ( ( B e. RR /\ A e. RR /\ _e <_ B ) /\ B < A ) -> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) )
12 11 ex 
 |-  ( ( B e. RR /\ A e. RR /\ _e <_ B ) -> ( B < A -> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) )
13 12 3expa 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ _e <_ B ) -> ( B < A -> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) )
14 13 an32s 
 |-  ( ( ( B e. RR /\ _e <_ B ) /\ A e. RR ) -> ( B < A -> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) )
15 14 adantrr 
 |-  ( ( ( B e. RR /\ _e <_ B ) /\ ( A e. RR /\ _e <_ A ) ) -> ( B < A -> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) )
16 15 ancoms 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( B < A -> ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) )
17 10 16 orim12d 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( ( A = B \/ B < A ) -> ( ( ( log ` B ) / B ) = ( ( log ` A ) / A ) \/ ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) ) )
18 17 con3d 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( -. ( ( ( log ` B ) / B ) = ( ( log ` A ) / A ) \/ ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) -> -. ( A = B \/ B < A ) ) )
19 simpl 
 |-  ( ( B e. RR /\ _e <_ B ) -> B e. RR )
20 epos 
 |-  0 < _e
21 0re 
 |-  0 e. RR
22 ere 
 |-  _e e. RR
23 ltletr 
 |-  ( ( 0 e. RR /\ _e e. RR /\ B e. RR ) -> ( ( 0 < _e /\ _e <_ B ) -> 0 < B ) )
24 21 22 23 mp3an12 
 |-  ( B e. RR -> ( ( 0 < _e /\ _e <_ B ) -> 0 < B ) )
25 20 24 mpani 
 |-  ( B e. RR -> ( _e <_ B -> 0 < B ) )
26 25 imp 
 |-  ( ( B e. RR /\ _e <_ B ) -> 0 < B )
27 19 26 elrpd 
 |-  ( ( B e. RR /\ _e <_ B ) -> B e. RR+ )
28 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
29 rerpdivcl 
 |-  ( ( ( log ` B ) e. RR /\ B e. RR+ ) -> ( ( log ` B ) / B ) e. RR )
30 28 29 mpancom 
 |-  ( B e. RR+ -> ( ( log ` B ) / B ) e. RR )
31 27 30 syl 
 |-  ( ( B e. RR /\ _e <_ B ) -> ( ( log ` B ) / B ) e. RR )
32 simpl 
 |-  ( ( A e. RR /\ _e <_ A ) -> A e. RR )
33 ltletr 
 |-  ( ( 0 e. RR /\ _e e. RR /\ A e. RR ) -> ( ( 0 < _e /\ _e <_ A ) -> 0 < A ) )
34 21 22 33 mp3an12 
 |-  ( A e. RR -> ( ( 0 < _e /\ _e <_ A ) -> 0 < A ) )
35 20 34 mpani 
 |-  ( A e. RR -> ( _e <_ A -> 0 < A ) )
36 35 imp 
 |-  ( ( A e. RR /\ _e <_ A ) -> 0 < A )
37 32 36 elrpd 
 |-  ( ( A e. RR /\ _e <_ A ) -> A e. RR+ )
38 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
39 rerpdivcl 
 |-  ( ( ( log ` A ) e. RR /\ A e. RR+ ) -> ( ( log ` A ) / A ) e. RR )
40 38 39 mpancom 
 |-  ( A e. RR+ -> ( ( log ` A ) / A ) e. RR )
41 37 40 syl 
 |-  ( ( A e. RR /\ _e <_ A ) -> ( ( log ` A ) / A ) e. RR )
42 axlttri 
 |-  ( ( ( ( log ` B ) / B ) e. RR /\ ( ( log ` A ) / A ) e. RR ) -> ( ( ( log ` B ) / B ) < ( ( log ` A ) / A ) <-> -. ( ( ( log ` B ) / B ) = ( ( log ` A ) / A ) \/ ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) ) )
43 31 41 42 syl2anr 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( ( ( log ` B ) / B ) < ( ( log ` A ) / A ) <-> -. ( ( ( log ` B ) / B ) = ( ( log ` A ) / A ) \/ ( ( log ` A ) / A ) < ( ( log ` B ) / B ) ) ) )
44 axlttri 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
45 44 ad2ant2r 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
46 18 43 45 3imtr4d 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( ( ( log ` B ) / B ) < ( ( log ` A ) / A ) -> A < B ) )
47 5 46 impbid 
 |-  ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A < B <-> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) ) )