| 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 ‘ 𝐴 ) / 𝐴 ) ) |