Metamath Proof Explorer

Theorem logdivlti

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 logdivlti 
|- ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> B e. RR )
2 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> _e <_ A )
3 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> A < B )
4 ere 
 |-  _e e. RR
5 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> A e. RR )
6 lelttr 
 |-  ( ( _e e. RR /\ A e. RR /\ B e. RR ) -> ( ( _e <_ A /\ A < B ) -> _e < B ) )
7 4 5 1 6 mp3an2i 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( _e <_ A /\ A < B ) -> _e < B ) )
8 2 3 7 mp2and 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> _e < B )
9 epos 
 |-  0 < _e
10 0re 
 |-  0 e. RR
11 lttr 
 |-  ( ( 0 e. RR /\ _e e. RR /\ B e. RR ) -> ( ( 0 < _e /\ _e < B ) -> 0 < B ) )
12 10 4 1 11 mp3an12i 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( 0 < _e /\ _e < B ) -> 0 < B ) )
13 9 12 mpani 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( _e < B -> 0 < B ) )
14 8 13 mpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> 0 < B )
15 1 14 elrpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> B e. RR+ )
16 ltletr 
 |-  ( ( 0 e. RR /\ _e e. RR /\ A e. RR ) -> ( ( 0 < _e /\ _e <_ A ) -> 0 < A ) )
17 10 4 5 16 mp3an12i 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( 0 < _e /\ _e <_ A ) -> 0 < A ) )
18 9 17 mpani 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( _e <_ A -> 0 < A ) )
19 2 18 mpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> 0 < A )
20 5 19 elrpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> A e. RR+ )
21 15 20 rpdivcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( B / A ) e. RR+ )
22 relogcl 
 |-  ( ( B / A ) e. RR+ -> ( log ` ( B / A ) ) e. RR )
23 21 22 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` ( B / A ) ) e. RR )
24 1 20 rerpdivcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( B / A ) e. RR )
25 1re 
 |-  1 e. RR
26 resubcl 
 |-  ( ( ( B / A ) e. RR /\ 1 e. RR ) -> ( ( B / A ) - 1 ) e. RR )
27 24 25 26 sylancl 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( B / A ) - 1 ) e. RR )
28 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
29 20 28 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` A ) e. RR )
30 27 29 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( ( B / A ) - 1 ) x. ( log ` A ) ) e. RR )
31 reeflog 
 |-  ( ( B / A ) e. RR+ -> ( exp ` ( log ` ( B / A ) ) ) = ( B / A ) )
32 21 31 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( exp ` ( log ` ( B / A ) ) ) = ( B / A ) )
33 ax-1cn 
 |-  1 e. CC
34 24 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( B / A ) e. CC )
35 pncan3 
 |-  ( ( 1 e. CC /\ ( B / A ) e. CC ) -> ( 1 + ( ( B / A ) - 1 ) ) = ( B / A ) )
36 33 34 35 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 + ( ( B / A ) - 1 ) ) = ( B / A ) )
37 32 36 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( exp ` ( log ` ( B / A ) ) ) = ( 1 + ( ( B / A ) - 1 ) ) )
38 5 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> A e. CC )
39 38 mulid2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 x. A ) = A )
40 39 3 eqbrtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 x. A ) < B )
41 1red 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> 1 e. RR )
42 ltmuldiv 
 |-  ( ( 1 e. RR /\ B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( 1 x. A ) < B <-> 1 < ( B / A ) ) )
43 41 1 5 19 42 syl112anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( 1 x. A ) < B <-> 1 < ( B / A ) ) )
44 40 43 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> 1 < ( B / A ) )
45 difrp 
 |-  ( ( 1 e. RR /\ ( B / A ) e. RR ) -> ( 1 < ( B / A ) <-> ( ( B / A ) - 1 ) e. RR+ ) )
46 25 24 45 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 < ( B / A ) <-> ( ( B / A ) - 1 ) e. RR+ ) )
47 44 46 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( B / A ) - 1 ) e. RR+ )
48 efgt1p 
 |-  ( ( ( B / A ) - 1 ) e. RR+ -> ( 1 + ( ( B / A ) - 1 ) ) < ( exp ` ( ( B / A ) - 1 ) ) )
49 47 48 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 + ( ( B / A ) - 1 ) ) < ( exp ` ( ( B / A ) - 1 ) ) )
50 37 49 eqbrtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( exp ` ( log ` ( B / A ) ) ) < ( exp ` ( ( B / A ) - 1 ) ) )
51 eflt 
 |-  ( ( ( log ` ( B / A ) ) e. RR /\ ( ( B / A ) - 1 ) e. RR ) -> ( ( log ` ( B / A ) ) < ( ( B / A ) - 1 ) <-> ( exp ` ( log ` ( B / A ) ) ) < ( exp ` ( ( B / A ) - 1 ) ) ) )
52 23 27 51 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` ( B / A ) ) < ( ( B / A ) - 1 ) <-> ( exp ` ( log ` ( B / A ) ) ) < ( exp ` ( ( B / A ) - 1 ) ) ) )
53 50 52 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` ( B / A ) ) < ( ( B / A ) - 1 ) )
54 27 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( B / A ) - 1 ) e. CC )
55 54 mulid1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( ( B / A ) - 1 ) x. 1 ) = ( ( B / A ) - 1 ) )
56 df-e 
 |-  _e = ( exp ` 1 )
57 reeflog 
 |-  ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
58 20 57 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( exp ` ( log ` A ) ) = A )
59 2 58 breqtrrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> _e <_ ( exp ` ( log ` A ) ) )
60 56 59 eqbrtrrid 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( exp ` 1 ) <_ ( exp ` ( log ` A ) ) )
61 efle 
 |-  ( ( 1 e. RR /\ ( log ` A ) e. RR ) -> ( 1 <_ ( log ` A ) <-> ( exp ` 1 ) <_ ( exp ` ( log ` A ) ) ) )
62 25 29 61 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 <_ ( log ` A ) <-> ( exp ` 1 ) <_ ( exp ` ( log ` A ) ) ) )
63 60 62 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> 1 <_ ( log ` A ) )
64 posdif 
 |-  ( ( 1 e. RR /\ ( B / A ) e. RR ) -> ( 1 < ( B / A ) <-> 0 < ( ( B / A ) - 1 ) ) )
65 25 24 64 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 < ( B / A ) <-> 0 < ( ( B / A ) - 1 ) ) )
66 44 65 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> 0 < ( ( B / A ) - 1 ) )
67 lemul2 
 |-  ( ( 1 e. RR /\ ( log ` A ) e. RR /\ ( ( ( B / A ) - 1 ) e. RR /\ 0 < ( ( B / A ) - 1 ) ) ) -> ( 1 <_ ( log ` A ) <-> ( ( ( B / A ) - 1 ) x. 1 ) <_ ( ( ( B / A ) - 1 ) x. ( log ` A ) ) ) )
68 41 29 27 66 67 syl112anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 <_ ( log ` A ) <-> ( ( ( B / A ) - 1 ) x. 1 ) <_ ( ( ( B / A ) - 1 ) x. ( log ` A ) ) ) )
69 63 68 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( ( B / A ) - 1 ) x. 1 ) <_ ( ( ( B / A ) - 1 ) x. ( log ` A ) ) )
70 55 69 eqbrtrrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( B / A ) - 1 ) <_ ( ( ( B / A ) - 1 ) x. ( log ` A ) ) )
71 23 27 30 53 70 ltletrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` ( B / A ) ) < ( ( ( B / A ) - 1 ) x. ( log ` A ) ) )
72 relogdiv 
 |-  ( ( B e. RR+ /\ A e. RR+ ) -> ( log ` ( B / A ) ) = ( ( log ` B ) - ( log ` A ) ) )
73 15 20 72 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` ( B / A ) ) = ( ( log ` B ) - ( log ` A ) ) )
74 1cnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> 1 e. CC )
75 29 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` A ) e. CC )
76 34 74 75 subdird 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( ( B / A ) - 1 ) x. ( log ` A ) ) = ( ( ( B / A ) x. ( log ` A ) ) - ( 1 x. ( log ` A ) ) ) )
77 1 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> B e. CC )
78 20 rpne0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> A =/= 0 )
79 77 38 75 78 div32d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( B / A ) x. ( log ` A ) ) = ( B x. ( ( log ` A ) / A ) ) )
80 75 mulid2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( 1 x. ( log ` A ) ) = ( log ` A ) )
81 79 80 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( ( B / A ) x. ( log ` A ) ) - ( 1 x. ( log ` A ) ) ) = ( ( B x. ( ( log ` A ) / A ) ) - ( log ` A ) ) )
82 76 81 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( ( B / A ) - 1 ) x. ( log ` A ) ) = ( ( B x. ( ( log ` A ) / A ) ) - ( log ` A ) ) )
83 71 73 82 3brtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) - ( log ` A ) ) < ( ( B x. ( ( log ` A ) / A ) ) - ( log ` A ) ) )
84 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
85 15 84 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` B ) e. RR )
86 29 20 rerpdivcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` A ) / A ) e. RR )
87 1 86 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( B x. ( ( log ` A ) / A ) ) e. RR )
88 85 87 29 ltsub1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) < ( B x. ( ( log ` A ) / A ) ) <-> ( ( log ` B ) - ( log ` A ) ) < ( ( B x. ( ( log ` A ) / A ) ) - ( log ` A ) ) ) )
89 83 88 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( log ` B ) < ( B x. ( ( log ` A ) / A ) ) )
90 85 86 15 ltdivmuld 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( ( log ` B ) / B ) < ( ( log ` A ) / A ) <-> ( log ` B ) < ( B x. ( ( log ` A ) / A ) ) ) )
91 89 90 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) )