Proof of Theorem logdivlti
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl2 1192 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) | 
| 2 |  | simpl3 1193 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e ≤ 𝐴) | 
| 3 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) | 
| 4 |  | ere 16126 | . . . . . . . . . . 11
⊢ e ∈
ℝ | 
| 5 |  | simpl1 1191 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) | 
| 6 |  | lelttr 11352 | . . . . . . . . . . 11
⊢ ((e
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → ((e ≤ 𝐴 ∧ 𝐴 < 𝐵) → e < 𝐵)) | 
| 7 | 4, 5, 1, 6 | mp3an2i 1467 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((e ≤ 𝐴 ∧ 𝐴 < 𝐵) → e < 𝐵)) | 
| 8 | 2, 3, 7 | mp2and 699 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e < 𝐵) | 
| 9 |  | epos 16244 | . . . . . . . . . 10
⊢ 0 <
e | 
| 10 |  | 0re 11264 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ | 
| 11 |  | lttr 11338 | . . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ e ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < e ∧ e
< 𝐵) → 0 < 𝐵)) | 
| 12 | 10, 4, 1, 11 | mp3an12i 1466 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((0 < e ∧ e < 𝐵) → 0 < 𝐵)) | 
| 13 | 9, 12 | mpani 696 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (e < 𝐵 → 0 < 𝐵)) | 
| 14 | 8, 13 | mpd 15 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < 𝐵) | 
| 15 | 1, 14 | elrpd 13075 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈
ℝ+) | 
| 16 |  | ltletr 11354 | . . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ e ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < e ∧ e
≤ 𝐴) → 0 < 𝐴)) | 
| 17 | 10, 4, 5, 16 | mp3an12i 1466 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((0 < e ∧ e ≤ 𝐴) → 0 < 𝐴)) | 
| 18 | 9, 17 | mpani 696 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (e ≤ 𝐴 → 0 < 𝐴)) | 
| 19 | 2, 18 | mpd 15 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < 𝐴) | 
| 20 | 5, 19 | elrpd 13075 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈
ℝ+) | 
| 21 | 15, 20 | rpdivcld 13095 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈
ℝ+) | 
| 22 |  | relogcl 26618 | . . . . . 6
⊢ ((𝐵 / 𝐴) ∈ ℝ+ →
(log‘(𝐵 / 𝐴)) ∈
ℝ) | 
| 23 | 21, 22 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) ∈ ℝ) | 
| 24 | 1, 20 | rerpdivcld 13109 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈ ℝ) | 
| 25 |  | 1re 11262 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 26 |  | resubcl 11574 | . . . . . 6
⊢ (((𝐵 / 𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝐵 / 𝐴) − 1) ∈
ℝ) | 
| 27 | 24, 25, 26 | sylancl 586 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℝ) | 
| 28 |  | relogcl 26618 | . . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) | 
| 29 | 20, 28 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐴) ∈ ℝ) | 
| 30 | 27, 29 | remulcld 11292 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) ∈
ℝ) | 
| 31 |  | reeflog 26623 | . . . . . . . . 9
⊢ ((𝐵 / 𝐴) ∈ ℝ+ →
(exp‘(log‘(𝐵 /
𝐴))) = (𝐵 / 𝐴)) | 
| 32 | 21, 31 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) = (𝐵 / 𝐴)) | 
| 33 |  | ax-1cn 11214 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 34 | 24 | recnd 11290 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈ ℂ) | 
| 35 |  | pncan3 11517 | . . . . . . . . 9
⊢ ((1
∈ ℂ ∧ (𝐵 /
𝐴) ∈ ℂ) →
(1 + ((𝐵 / 𝐴) − 1)) = (𝐵 / 𝐴)) | 
| 36 | 33, 34, 35 | sylancr 587 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 + ((𝐵 / 𝐴) − 1)) = (𝐵 / 𝐴)) | 
| 37 | 32, 36 | eqtr4d 2779 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) = (1 + ((𝐵 / 𝐴) − 1))) | 
| 38 | 5 | recnd 11290 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) | 
| 39 | 38 | mullidd 11280 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · 𝐴) = 𝐴) | 
| 40 | 39, 3 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · 𝐴) < 𝐵) | 
| 41 |  | 1red 11263 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ∈ ℝ) | 
| 42 |  | ltmuldiv 12142 | . . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ ∧ (𝐴
∈ ℝ ∧ 0 < 𝐴)) → ((1 · 𝐴) < 𝐵 ↔ 1 < (𝐵 / 𝐴))) | 
| 43 | 41, 1, 5, 19, 42 | syl112anc 1375 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((1 · 𝐴) < 𝐵 ↔ 1 < (𝐵 / 𝐴))) | 
| 44 | 40, 43 | mpbid 232 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 < (𝐵 / 𝐴)) | 
| 45 |  | difrp 13074 | . . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (𝐵 /
𝐴) ∈ ℝ) →
(1 < (𝐵 / 𝐴) ↔ ((𝐵 / 𝐴) − 1) ∈
ℝ+)) | 
| 46 | 25, 24, 45 | sylancr 587 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 < (𝐵 / 𝐴) ↔ ((𝐵 / 𝐴) − 1) ∈
ℝ+)) | 
| 47 | 44, 46 | mpbid 232 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℝ+) | 
| 48 |  | efgt1p 16152 | . . . . . . . 8
⊢ (((𝐵 / 𝐴) − 1) ∈ ℝ+
→ (1 + ((𝐵 / 𝐴) − 1)) <
(exp‘((𝐵 / 𝐴) − 1))) | 
| 49 | 47, 48 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 + ((𝐵 / 𝐴) − 1)) < (exp‘((𝐵 / 𝐴) − 1))) | 
| 50 | 37, 49 | eqbrtrd 5164 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) < (exp‘((𝐵 / 𝐴) − 1))) | 
| 51 |  | eflt 16154 | . . . . . . 7
⊢
(((log‘(𝐵 /
𝐴)) ∈ ℝ ∧
((𝐵 / 𝐴) − 1) ∈ ℝ) →
((log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1) ↔
(exp‘(log‘(𝐵 /
𝐴))) <
(exp‘((𝐵 / 𝐴) − 1)))) | 
| 52 | 23, 27, 51 | syl2anc 584 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1) ↔
(exp‘(log‘(𝐵 /
𝐴))) <
(exp‘((𝐵 / 𝐴) − 1)))) | 
| 53 | 50, 52 | mpbird 257 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1)) | 
| 54 | 27 | recnd 11290 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℂ) | 
| 55 | 54 | mulridd 11279 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · 1) = ((𝐵 / 𝐴) − 1)) | 
| 56 |  | df-e 16105 | . . . . . . . . 9
⊢ e =
(exp‘1) | 
| 57 |  | reeflog 26623 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (exp‘(log‘𝐴)) = 𝐴) | 
| 58 | 20, 57 | syl 17 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘𝐴)) = 𝐴) | 
| 59 | 2, 58 | breqtrrd 5170 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e ≤ (exp‘(log‘𝐴))) | 
| 60 | 56, 59 | eqbrtrrid 5178 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘1) ≤
(exp‘(log‘𝐴))) | 
| 61 |  | efle 16155 | . . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (1 ≤
(log‘𝐴) ↔
(exp‘1) ≤ (exp‘(log‘𝐴)))) | 
| 62 | 25, 29, 61 | sylancr 587 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 ≤ (log‘𝐴) ↔ (exp‘1) ≤
(exp‘(log‘𝐴)))) | 
| 63 | 60, 62 | mpbird 257 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ≤ (log‘𝐴)) | 
| 64 |  | posdif 11757 | . . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (𝐵 /
𝐴) ∈ ℝ) →
(1 < (𝐵 / 𝐴) ↔ 0 < ((𝐵 / 𝐴) − 1))) | 
| 65 | 25, 24, 64 | sylancr 587 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 < (𝐵 / 𝐴) ↔ 0 < ((𝐵 / 𝐴) − 1))) | 
| 66 | 44, 65 | mpbid 232 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < ((𝐵 / 𝐴) − 1)) | 
| 67 |  | lemul2 12121 | . . . . . . . 8
⊢ ((1
∈ ℝ ∧ (log‘𝐴) ∈ ℝ ∧ (((𝐵 / 𝐴) − 1) ∈ ℝ ∧ 0 <
((𝐵 / 𝐴) − 1))) → (1 ≤
(log‘𝐴) ↔
(((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴)))) | 
| 68 | 41, 29, 27, 66, 67 | syl112anc 1375 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 ≤ (log‘𝐴) ↔ (((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴)))) | 
| 69 | 63, 68 | mpbid 232 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴))) | 
| 70 | 55, 69 | eqbrtrrd 5166 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴))) | 
| 71 | 23, 27, 30, 53, 70 | ltletrd 11422 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) < (((𝐵 / 𝐴) − 1) · (log‘𝐴))) | 
| 72 |  | relogdiv 26636 | . . . . 5
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 ∈
ℝ+) → (log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴))) | 
| 73 | 15, 20, 72 | syl2anc 584 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴))) | 
| 74 |  | 1cnd 11257 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ∈ ℂ) | 
| 75 | 29 | recnd 11290 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐴) ∈ ℂ) | 
| 76 | 34, 74, 75 | subdird 11721 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) = (((𝐵 / 𝐴) · (log‘𝐴)) − (1 · (log‘𝐴)))) | 
| 77 | 1 | recnd 11290 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) | 
| 78 | 20 | rpne0d 13083 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ≠ 0) | 
| 79 | 77, 38, 75, 78 | div32d 12067 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) · (log‘𝐴)) = (𝐵 · ((log‘𝐴) / 𝐴))) | 
| 80 | 75 | mullidd 11280 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · (log‘𝐴)) = (log‘𝐴)) | 
| 81 | 79, 80 | oveq12d 7450 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) · (log‘𝐴)) − (1 · (log‘𝐴))) = ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) | 
| 82 | 76, 81 | eqtrd 2776 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) = ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) | 
| 83 | 71, 73, 82 | 3brtr3d 5173 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) − (log‘𝐴)) < ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) | 
| 84 |  | relogcl 26618 | . . . . 5
⊢ (𝐵 ∈ ℝ+
→ (log‘𝐵) ∈
ℝ) | 
| 85 | 15, 84 | syl 17 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐵) ∈ ℝ) | 
| 86 | 29, 20 | rerpdivcld 13109 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐴) / 𝐴) ∈ ℝ) | 
| 87 | 1, 86 | remulcld 11292 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 · ((log‘𝐴) / 𝐴)) ∈ ℝ) | 
| 88 | 85, 87, 29 | ltsub1d 11873 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴)) ↔ ((log‘𝐵) − (log‘𝐴)) < ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴)))) | 
| 89 | 83, 88 | mpbird 257 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴))) | 
| 90 | 85, 86, 15 | ltdivmuld 13129 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴) ↔ (log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴)))) | 
| 91 | 89, 90 | mpbird 257 | 1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) |