Proof of Theorem logdivlti
Step | Hyp | Ref
| Expression |
1 | | simpl2 986 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
2 | | simpl3 987 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e ≤ 𝐴) |
3 | | simpr 109 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
4 | | ere 11544 |
. . . . . . . . . . 11
⊢ e ∈
ℝ |
5 | | simpl1 985 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
6 | | lelttr 7944 |
. . . . . . . . . . 11
⊢ ((e
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → ((e ≤ 𝐴 ∧ 𝐴 < 𝐵) → e < 𝐵)) |
7 | 4, 5, 1, 6 | mp3an2i 1321 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((e ≤ 𝐴 ∧ 𝐴 < 𝐵) → e < 𝐵)) |
8 | 2, 3, 7 | mp2and 430 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e < 𝐵) |
9 | | epos 11654 |
. . . . . . . . . 10
⊢ 0 <
e |
10 | | 0re 7857 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
11 | | lttr 7930 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ e ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < e ∧ e
< 𝐵) → 0 < 𝐵)) |
12 | 10, 4, 1, 11 | mp3an12i 1320 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((0 < e ∧ e < 𝐵) → 0 < 𝐵)) |
13 | 9, 12 | mpani 427 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (e < 𝐵 → 0 < 𝐵)) |
14 | 8, 13 | mpd 13 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < 𝐵) |
15 | 1, 14 | elrpd 9578 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈
ℝ+) |
16 | | ltletr 7945 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ e ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < e ∧ e
≤ 𝐴) → 0 < 𝐴)) |
17 | 10, 4, 5, 16 | mp3an12i 1320 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((0 < e ∧ e ≤ 𝐴) → 0 < 𝐴)) |
18 | 9, 17 | mpani 427 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (e ≤ 𝐴 → 0 < 𝐴)) |
19 | 2, 18 | mpd 13 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < 𝐴) |
20 | 5, 19 | elrpd 9578 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈
ℝ+) |
21 | 15, 20 | rpdivcld 9599 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈
ℝ+) |
22 | | relogcl 13122 |
. . . . . 6
⊢ ((𝐵 / 𝐴) ∈ ℝ+ →
(log‘(𝐵 / 𝐴)) ∈
ℝ) |
23 | 21, 22 | syl 14 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) ∈ ℝ) |
24 | 1, 20 | rerpdivcld 9613 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈ ℝ) |
25 | | 1re 7856 |
. . . . . 6
⊢ 1 ∈
ℝ |
26 | | resubcl 8118 |
. . . . . 6
⊢ (((𝐵 / 𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝐵 / 𝐴) − 1) ∈
ℝ) |
27 | 24, 25, 26 | sylancl 410 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℝ) |
28 | | relogcl 13122 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
29 | 20, 28 | syl 14 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐴) ∈ ℝ) |
30 | 27, 29 | remulcld 7887 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) ∈
ℝ) |
31 | | reeflog 13123 |
. . . . . . . . 9
⊢ ((𝐵 / 𝐴) ∈ ℝ+ →
(exp‘(log‘(𝐵 /
𝐴))) = (𝐵 / 𝐴)) |
32 | 21, 31 | syl 14 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) = (𝐵 / 𝐴)) |
33 | | ax-1cn 7804 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
34 | 24 | recnd 7885 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 / 𝐴) ∈ ℂ) |
35 | | pncan3 8062 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ (𝐵 /
𝐴) ∈ ℂ) →
(1 + ((𝐵 / 𝐴) − 1)) = (𝐵 / 𝐴)) |
36 | 33, 34, 35 | sylancr 411 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 + ((𝐵 / 𝐴) − 1)) = (𝐵 / 𝐴)) |
37 | 32, 36 | eqtr4d 2190 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) = (1 + ((𝐵 / 𝐴) − 1))) |
38 | 5 | recnd 7885 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) |
39 | 38 | mulid2d 7875 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · 𝐴) = 𝐴) |
40 | 39, 3 | eqbrtrd 3982 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · 𝐴) < 𝐵) |
41 | | 1red 7872 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ∈ ℝ) |
42 | | ltmuldiv 8724 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ ∧ (𝐴
∈ ℝ ∧ 0 < 𝐴)) → ((1 · 𝐴) < 𝐵 ↔ 1 < (𝐵 / 𝐴))) |
43 | 41, 1, 5, 19, 42 | syl112anc 1221 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((1 · 𝐴) < 𝐵 ↔ 1 < (𝐵 / 𝐴))) |
44 | 40, 43 | mpbid 146 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 < (𝐵 / 𝐴)) |
45 | | difrp 9577 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (𝐵 /
𝐴) ∈ ℝ) →
(1 < (𝐵 / 𝐴) ↔ ((𝐵 / 𝐴) − 1) ∈
ℝ+)) |
46 | 25, 24, 45 | sylancr 411 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 < (𝐵 / 𝐴) ↔ ((𝐵 / 𝐴) − 1) ∈
ℝ+)) |
47 | 44, 46 | mpbid 146 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℝ+) |
48 | | efgt1p 11570 |
. . . . . . . 8
⊢ (((𝐵 / 𝐴) − 1) ∈ ℝ+
→ (1 + ((𝐵 / 𝐴) − 1)) <
(exp‘((𝐵 / 𝐴) − 1))) |
49 | 47, 48 | syl 14 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 + ((𝐵 / 𝐴) − 1)) < (exp‘((𝐵 / 𝐴) − 1))) |
50 | 37, 49 | eqbrtrd 3982 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘(𝐵 / 𝐴))) < (exp‘((𝐵 / 𝐴) − 1))) |
51 | | eflt 13035 |
. . . . . . 7
⊢
(((log‘(𝐵 /
𝐴)) ∈ ℝ ∧
((𝐵 / 𝐴) − 1) ∈ ℝ) →
((log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1) ↔
(exp‘(log‘(𝐵 /
𝐴))) <
(exp‘((𝐵 / 𝐴) − 1)))) |
52 | 23, 27, 51 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1) ↔
(exp‘(log‘(𝐵 /
𝐴))) <
(exp‘((𝐵 / 𝐴) − 1)))) |
53 | 50, 52 | mpbird 166 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) < ((𝐵 / 𝐴) − 1)) |
54 | 27 | recnd 7885 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ∈
ℂ) |
55 | 54 | mulid1d 7874 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · 1) = ((𝐵 / 𝐴) − 1)) |
56 | | df-e 11523 |
. . . . . . . . 9
⊢ e =
(exp‘1) |
57 | | reeflog 13123 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (exp‘(log‘𝐴)) = 𝐴) |
58 | 20, 57 | syl 14 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘(log‘𝐴)) = 𝐴) |
59 | 2, 58 | breqtrrd 3988 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → e ≤ (exp‘(log‘𝐴))) |
60 | 56, 59 | eqbrtrrid 3996 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (exp‘1) ≤
(exp‘(log‘𝐴))) |
61 | | efle 13036 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (1 ≤
(log‘𝐴) ↔
(exp‘1) ≤ (exp‘(log‘𝐴)))) |
62 | 25, 29, 61 | sylancr 411 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 ≤ (log‘𝐴) ↔ (exp‘1) ≤
(exp‘(log‘𝐴)))) |
63 | 60, 62 | mpbird 166 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ≤ (log‘𝐴)) |
64 | | posdif 8309 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (𝐵 /
𝐴) ∈ ℝ) →
(1 < (𝐵 / 𝐴) ↔ 0 < ((𝐵 / 𝐴) − 1))) |
65 | 25, 24, 64 | sylancr 411 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 < (𝐵 / 𝐴) ↔ 0 < ((𝐵 / 𝐴) − 1))) |
66 | 44, 65 | mpbid 146 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 0 < ((𝐵 / 𝐴) − 1)) |
67 | | lemul2 8707 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (log‘𝐴) ∈ ℝ ∧ (((𝐵 / 𝐴) − 1) ∈ ℝ ∧ 0 <
((𝐵 / 𝐴) − 1))) → (1 ≤
(log‘𝐴) ↔
(((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴)))) |
68 | 41, 29, 27, 66, 67 | syl112anc 1221 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 ≤ (log‘𝐴) ↔ (((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴)))) |
69 | 63, 68 | mpbid 146 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴))) |
70 | 55, 69 | eqbrtrrd 3984 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) − 1) ≤ (((𝐵 / 𝐴) − 1) · (log‘𝐴))) |
71 | 23, 27, 30, 53, 70 | ltletrd 8277 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) < (((𝐵 / 𝐴) − 1) · (log‘𝐴))) |
72 | | relogdiv 13130 |
. . . . 5
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 ∈
ℝ+) → (log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴))) |
73 | 15, 20, 72 | syl2anc 409 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘(𝐵 / 𝐴)) = ((log‘𝐵) − (log‘𝐴))) |
74 | | 1cnd 7873 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 1 ∈ ℂ) |
75 | 29 | recnd 7885 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐴) ∈ ℂ) |
76 | 34, 74, 75 | subdird 8269 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) = (((𝐵 / 𝐴) · (log‘𝐴)) − (1 · (log‘𝐴)))) |
77 | 1 | recnd 7885 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) |
78 | 20 | rpap0d 9587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → 𝐴 # 0) |
79 | 77, 38, 75, 78 | div32apd 8666 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((𝐵 / 𝐴) · (log‘𝐴)) = (𝐵 · ((log‘𝐴) / 𝐴))) |
80 | 75 | mulid2d 7875 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (1 · (log‘𝐴)) = (log‘𝐴)) |
81 | 79, 80 | oveq12d 5832 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) · (log‘𝐴)) − (1 · (log‘𝐴))) = ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) |
82 | 76, 81 | eqtrd 2187 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((𝐵 / 𝐴) − 1) · (log‘𝐴)) = ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) |
83 | 71, 73, 82 | 3brtr3d 3991 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) − (log‘𝐴)) < ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴))) |
84 | | relogcl 13122 |
. . . . 5
⊢ (𝐵 ∈ ℝ+
→ (log‘𝐵) ∈
ℝ) |
85 | 15, 84 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐵) ∈ ℝ) |
86 | 29, 20 | rerpdivcld 9613 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐴) / 𝐴) ∈ ℝ) |
87 | 1, 86 | remulcld 7887 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (𝐵 · ((log‘𝐴) / 𝐴)) ∈ ℝ) |
88 | 85, 87, 29 | ltsub1d 8408 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴)) ↔ ((log‘𝐵) − (log‘𝐴)) < ((𝐵 · ((log‘𝐴) / 𝐴)) − (log‘𝐴)))) |
89 | 83, 88 | mpbird 166 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴))) |
90 | 85, 86, 15 | ltdivmuld 9633 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → (((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴) ↔ (log‘𝐵) < (𝐵 · ((log‘𝐴) / 𝐴)))) |
91 | 89, 90 | mpbird 166 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤
𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) |