This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) )

Proof

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