Proof of Theorem logdivlti
Step | Hyp | Ref
| Expression |
1 | | simpl2 1058 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
2 | | simpl3 1059 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e ≤ 𝐴) |
3 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
4 | | simpl1 1057 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
5 | | ere 14658 |
. . . . . . . . . . . 12
⊢ e ∈
ℝ |
6 | | lelttr 10007 |
. . . . . . . . . . . 12
⊢ ((e
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → ((e ≤ 𝐴 ∧ 𝐴 < 𝐵) → e < 𝐵)) |
7 | 5, 6 | mp3an1 1403 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((e ≤
𝐴 ∧ 𝐴 < 𝐵) → e < 𝐵)) |
8 | 4, 1, 7 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((e ≤ 𝐴 ∧ 𝐴 < 𝐵) → e < 𝐵)) |
9 | 2, 3, 8 | mp2and 711 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e < 𝐵) |
10 | | epos 14774 |
. . . . . . . . . 10
⊢ 0 <
e |
11 | | 0re 9919 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
12 | | lttr 9993 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ e ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < e ∧ e
< 𝐵) → 0 < 𝐵)) |
13 | 11, 5, 12 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → ((0 <
e ∧ e < 𝐵) → 0
< 𝐵)) |
14 | 1, 13 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((0 < e ∧ e < 𝐵) → 0 < 𝐵)) |
15 | 10, 14 | mpani 708 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (e < 𝐵 → 0 < 𝐵)) |
16 | 9, 15 | mpd 15 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < 𝐵) |
17 | 1, 16 | elrpd 11745 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈
ℝ+) |
18 | | ltletr 10008 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ e ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < e ∧ e
≤ 𝐴) → 0 < 𝐴)) |
19 | 11, 5, 18 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → ((0 <
e ∧ e ≤ 𝐴) → 0
< 𝐴)) |
20 | 4, 19 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((0 < e ∧ e ≤ 𝐴) → 0 < 𝐴)) |
21 | 10, 20 | mpani 708 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (e ≤ 𝐴 → 0 < 𝐴)) |
22 | 2, 21 | mpd 15 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < 𝐴) |
23 | 4, 22 | elrpd 11745 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈
ℝ+) |
24 | 17, 23 | rpdivcld 11765 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈
ℝ+) |
25 | | relogcl 24126 |
. . . . . 6
⊢ ((𝐵 / 𝐴) ∈ ℝ+ →
(log‘(𝐵 / 𝐴)) ∈
ℝ) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) ∈ ℝ) |
27 | 1, 23 | rerpdivcld 11779 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈ ℝ) |
28 | | 1re 9918 |
. . . . . 6
⊢ 1 ∈
ℝ |
29 | | resubcl 10224 |
. . . . . 6
⊢ (((𝐵 / 𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝐵 / 𝐴) − 1) ∈
ℝ) |
30 | 27, 28, 29 | sylancl 693 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℝ) |
31 | | relogcl 24126 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
32 | 23, 31 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐴) ∈ ℝ) |
33 | 30, 32 | remulcld 9949 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) ∈
ℝ) |
34 | | reeflog 24131 |
. . . . . . . . 9
⊢ ((𝐵 / 𝐴) ∈ ℝ+ →
(exp‘(log‘(𝐵 /
𝐴))) = (𝐵 / 𝐴)) |
35 | 24, 34 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) = (𝐵 / 𝐴)) |
36 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
37 | 27 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈ ℂ) |
38 | | pncan3 10168 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ (𝐵 /
𝐴) ∈ ℂ) →
(1 + ((𝐵 / 𝐴) − 1)) = (𝐵 / 𝐴)) |
39 | 36, 37, 38 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 + ((𝐵 / 𝐴) − 1)) = (𝐵 / 𝐴)) |
40 | 35, 39 | eqtr4d 2647 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) = (1 + ((𝐵 / 𝐴) − 1))) |
41 | 4 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) |
42 | 41 | mulid2d 9937 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · 𝐴) = 𝐴) |
43 | 42, 3 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · 𝐴) < 𝐵) |
44 | | 1red 9934 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ∈ ℝ) |
45 | | ltmuldiv 10775 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ ∧ (𝐴
∈ ℝ ∧ 0 < 𝐴)) → ((1 · 𝐴) < 𝐵 ↔ 1 < (𝐵 / 𝐴))) |
46 | 44, 1, 4, 22, 45 | syl112anc 1322 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((1 · 𝐴) < 𝐵 ↔ 1 < (𝐵 / 𝐴))) |
47 | 43, 46 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 < (𝐵 / 𝐴)) |
48 | | difrp 11744 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (𝐵 /
𝐴) ∈ ℝ) →
(1 < (𝐵 / 𝐴) ↔ ((𝐵 / 𝐴) − 1) ∈
ℝ+)) |
49 | 28, 27, 48 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 < (𝐵 / 𝐴) ↔ ((𝐵 / 𝐴) − 1) ∈
ℝ+)) |
50 | 47, 49 | mpbid 221 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℝ+) |
51 | | efgt1p 14684 |
. . . . . . . 8
⊢ (((𝐵 / 𝐴) − 1) ∈ ℝ+
→ (1 + ((𝐵 / 𝐴) − 1)) <
(exp‘((𝐵 / 𝐴) − 1))) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 + ((𝐵 / 𝐴) − 1)) < (exp‘((𝐵 / 𝐴) − 1))) |
53 | 40, 52 | eqbrtrd 4605 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) < (exp‘((𝐵 / 𝐴) − 1))) |
54 | | eflt 14686 |
. . . . . . 7
⊢
(((log‘(𝐵 /
𝐴)) ∈ ℝ ∧
((𝐵 / 𝐴) − 1) ∈ ℝ) →
((log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1) ↔
(exp‘(log‘(𝐵 /
𝐴))) <
(exp‘((𝐵 / 𝐴) − 1)))) |
55 | 26, 30, 54 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1) ↔
(exp‘(log‘(𝐵 /
𝐴))) <
(exp‘((𝐵 / 𝐴) − 1)))) |
56 | 53, 55 | mpbird 246 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1)) |
57 | 30 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℂ) |
58 | 57 | mulid1d 9936 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · 1) = ((𝐵 / 𝐴) − 1)) |
59 | | df-e 14638 |
. . . . . . . . 9
⊢ e =
(exp‘1) |
60 | | reeflog 24131 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (exp‘(log‘𝐴)) = 𝐴) |
61 | 23, 60 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘𝐴)) = 𝐴) |
62 | 2, 61 | breqtrrd 4611 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e ≤ (exp‘(log‘𝐴))) |
63 | 59, 62 | syl5eqbrr 4619 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘1) ≤
(exp‘(log‘𝐴))) |
64 | | efle 14687 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (1 ≤
(log‘𝐴) ↔
(exp‘1) ≤ (exp‘(log‘𝐴)))) |
65 | 28, 32, 64 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 ≤ (log‘𝐴) ↔ (exp‘1) ≤
(exp‘(log‘𝐴)))) |
66 | 63, 65 | mpbird 246 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ≤ (log‘𝐴)) |
67 | | posdif 10400 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (𝐵 /
𝐴) ∈ ℝ) →
(1 < (𝐵 / 𝐴) ↔ 0 < ((𝐵 / 𝐴) − 1))) |
68 | 28, 27, 67 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 < (𝐵 / 𝐴) ↔ 0 < ((𝐵 / 𝐴) − 1))) |
69 | 47, 68 | mpbid 221 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < ((𝐵 / 𝐴) − 1)) |
70 | | lemul2 10755 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (log‘𝐴) ∈ ℝ ∧ (((𝐵 / 𝐴) − 1) ∈ ℝ ∧ 0 <
((𝐵 / 𝐴) − 1))) → (1 ≤
(log‘𝐴) ↔
(((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴)))) |
71 | 44, 32, 30, 69, 70 | syl112anc 1322 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 ≤ (log‘𝐴) ↔ (((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴)))) |
72 | 66, 71 | mpbid 221 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴))) |
73 | 58, 72 | eqbrtrrd 4607 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴))) |
74 | 26, 30, 33, 56, 73 | ltletrd 10076 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) < (((𝐵 / 𝐴) − 1) · (log‘𝐴))) |
75 | | relogdiv 24143 |
. . . . 5
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 ∈
ℝ+) → (log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴))) |
76 | 17, 23, 75 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴))) |
77 | | 1cnd 9935 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ∈ ℂ) |
78 | 32 | recnd 9947 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐴) ∈ ℂ) |
79 | 37, 77, 78 | subdird 10366 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) = (((𝐵 / 𝐴) · (log‘𝐴)) − (1 · (log‘𝐴)))) |
80 | 1 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) |
81 | 23 | rpne0d 11753 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ≠ 0) |
82 | 80, 41, 78, 81 | div32d 10703 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) · (log‘𝐴)) = (𝐵 · ((log‘𝐴) / 𝐴))) |
83 | 78 | mulid2d 9937 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · (log‘𝐴)) = (log‘𝐴)) |
84 | 82, 83 | oveq12d 6567 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) · (log‘𝐴)) − (1 · (log‘𝐴))) = ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) |
85 | 79, 84 | eqtrd 2644 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) = ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) |
86 | 74, 76, 85 | 3brtr3d 4614 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) − (log‘𝐴)) < ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) |
87 | | relogcl 24126 |
. . . . 5
⊢ (𝐵 ∈ ℝ+
→ (log‘𝐵) ∈
ℝ) |
88 | 17, 87 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐵) ∈ ℝ) |
89 | 32, 23 | rerpdivcld 11779 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐴) / 𝐴) ∈ ℝ) |
90 | 1, 89 | remulcld 9949 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 · ((log‘𝐴) / 𝐴)) ∈ ℝ) |
91 | 88, 90, 32 | ltsub1d 10515 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴)) ↔ ((log‘𝐵) − (log‘𝐴)) < ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴)))) |
92 | 86, 91 | mpbird 246 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴))) |
93 | 88, 89, 17 | ltdivmuld 11799 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴) ↔ (log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴)))) |
94 | 92, 93 | mpbird 246 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) |