Step | Hyp | Ref
| Expression |
1 | | 1re 10984 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
2 | | elicopnf 13186 |
. . . . . . . . 9
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
3 | 1, 2 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
4 | 3 | simprbda 499 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 𝑥 ∈ ℝ) |
5 | | 1rp 12743 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 1 ∈ ℝ+) |
7 | 3 | simplbda 500 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 1 ≤ 𝑥) |
8 | 4, 6, 7 | rpgecld 12820 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 𝑥 ∈ ℝ+) |
9 | 8 | ex 413 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) → 𝑥
∈ ℝ+)) |
10 | 9 | ssrdv 3928 |
. . . 4
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ+) |
11 | | rpssre 12746 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
12 | 10, 11 | sstrdi 3934 |
. . 3
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ) |
13 | 1 | a1i 11 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ) |
14 | | fzfid 13702 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
15 | | elfznn 13294 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
16 | 15 | adantl 482 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
17 | | vmacl 26276 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
19 | 18, 16 | nndivred 12036 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
20 | 14, 19 | fsumrecl 15455 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
21 | 8 | relogcld 25787 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (log‘𝑥) ∈ ℝ) |
22 | 20, 21 | resubcld 11412 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ) |
23 | 22 | recnd 11012 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
24 | | vmadivsum 26639 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
25 | 24 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
26 | 10, 25 | o1res2 15281 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
27 | | fzfid 13702 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (1...(⌊‘𝑦)) ∈ Fin) |
28 | | elfznn 13294 |
. . . . . . . 8
⊢ (𝑛 ∈
(1...(⌊‘𝑦))
→ 𝑛 ∈
ℕ) |
29 | 28 | adantl 482 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℕ) |
30 | 29, 17 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑛) ∈
ℝ) |
31 | 30, 29 | nndivred 12036 |
. . . . 5
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
32 | 27, 31 | fsumrecl 15455 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
33 | | simprl 768 |
. . . . . 6
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 𝑦 ∈ ℝ) |
34 | 5 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 1 ∈
ℝ+) |
35 | | simprr 770 |
. . . . . 6
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 1 ≤ 𝑦) |
36 | 33, 34, 35 | rpgecld 12820 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 𝑦 ∈ ℝ+) |
37 | 36 | relogcld 25787 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (log‘𝑦) ∈ ℝ) |
38 | 32, 37 | readdcld 11013 |
. . 3
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) / 𝑛) + (log‘𝑦)) ∈ ℝ) |
39 | 22 | adantr 481 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ) |
40 | 39 | recnd 11012 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
41 | 40 | abscld 15157 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ ℝ) |
42 | 20 | adantr 481 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
43 | 8 | adantr 481 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ+) |
44 | 43 | relogcld 25787 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ∈ ℝ) |
45 | 42, 44 | readdcld 11013 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) + (log‘𝑥)) ∈ ℝ) |
46 | 38 | ad2ant2r 744 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) / 𝑛) + (log‘𝑦)) ∈ ℝ) |
47 | 42 | recnd 11012 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
48 | 44 | recnd 11012 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ∈ ℂ) |
49 | 47, 48 | abs2dif2d 15179 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) + (abs‘(log‘𝑥)))) |
50 | 16 | nnrpd 12779 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
51 | | vmage0 26279 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
52 | 16, 51 | syl 17 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑛)) |
53 | 18, 50, 52 | divge0d 12821 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
54 | 14, 19, 53 | fsumge0 15516 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) |
55 | 54 | adantr 481 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) |
56 | 42, 55 | absidd 15143 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) |
57 | 21 | adantr 481 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ∈ ℝ) |
58 | 4 | adantr 481 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ) |
59 | 7 | adantr 481 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 1 ≤ 𝑥) |
60 | 58, 59 | logge0d 25794 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (log‘𝑥)) |
61 | 57, 60 | absidd 15143 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(log‘𝑥)) = (log‘𝑥)) |
62 | 56, 61 | oveq12d 7302 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) + (abs‘(log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) + (log‘𝑥))) |
63 | 49, 62 | breqtrd 5101 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) + (log‘𝑥))) |
64 | 32 | ad2ant2r 744 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
65 | 36 | ad2ant2r 744 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ+) |
66 | 65 | relogcld 25787 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑦) ∈ ℝ) |
67 | | fzfid 13702 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (1...(⌊‘𝑦)) ∈ Fin) |
68 | 28 | adantl 482 |
. . . . . . . 8
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℕ) |
69 | 68, 17 | syl 17 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑛) ∈
ℝ) |
70 | 69, 68 | nndivred 12036 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
71 | 68 | nnrpd 12779 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℝ+) |
72 | 68, 51 | syl 17 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤
(Λ‘𝑛)) |
73 | 69, 71, 72 | divge0d 12821 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
74 | | simprll 776 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ) |
75 | | simprr 770 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦) |
76 | 58, 74, 75 | ltled 11132 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≤ 𝑦) |
77 | | flword2 13542 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (⌊‘𝑦) ∈
(ℤ≥‘(⌊‘𝑥))) |
78 | 58, 74, 76, 77 | syl3anc 1370 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (⌊‘𝑦) ∈
(ℤ≥‘(⌊‘𝑥))) |
79 | | fzss2 13305 |
. . . . . . 7
⊢
((⌊‘𝑦)
∈ (ℤ≥‘(⌊‘𝑥)) → (1...(⌊‘𝑥)) ⊆
(1...(⌊‘𝑦))) |
80 | 78, 79 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (1...(⌊‘𝑥)) ⊆
(1...(⌊‘𝑦))) |
81 | 67, 70, 73, 80 | fsumless 15517 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) / 𝑛)) |
82 | 74, 43, 76 | rpgecld 12820 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ+) |
83 | 43, 82 | logled 25791 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 ≤ 𝑦 ↔ (log‘𝑥) ≤ (log‘𝑦))) |
84 | 76, 83 | mpbid 231 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ≤ (log‘𝑦)) |
85 | 42, 44, 64, 66, 81, 84 | le2addd 11603 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) + (log‘𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) / 𝑛) + (log‘𝑦))) |
86 | 41, 45, 46, 63, 85 | letrd 11141 |
. . 3
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) / 𝑛) + (log‘𝑦))) |
87 | 12, 13, 23, 26, 38, 86 | o1bddrp 15260 |
. 2
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑥 ∈
(1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐) |
88 | 87 | mptru 1546 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑥 ∈
(1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐 |