Step | Hyp | Ref
| Expression |
1 | | 1re 10732 |
. . . . . . 7
⊢ 1 ∈
ℝ |
2 | | elicopnf 12932 |
. . . . . . 7
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
4 | 3 | simprbda 502 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 𝑥 ∈ ℝ) |
5 | 4 | ex 416 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) → 𝑥
∈ ℝ)) |
6 | 5 | ssrdv 3893 |
. . 3
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ) |
7 | 1 | a1i 11 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ) |
8 | | fzfid 13445 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
9 | | elfznn 13040 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
10 | 9 | adantl 485 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
11 | | vmacl 25868 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
13 | 10 | nnrpd 12525 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
14 | 13 | relogcld 25379 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈
ℝ) |
15 | 4 | adantr 484 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ) |
16 | 15, 10 | nndivred 11783 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ) |
17 | | chpcl 25874 |
. . . . . . . . . 10
⊢ ((𝑥 / 𝑛) ∈ ℝ → (ψ‘(𝑥 / 𝑛)) ∈ ℝ) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑛)) ∈ ℝ) |
19 | 14, 18 | readdcld 10761 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))) ∈ ℝ) |
20 | 12, 19 | remulcld 10762 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛)))) ∈
ℝ) |
21 | 8, 20 | fsumrecl 15197 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ) |
22 | | 1rp 12489 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
23 | 22 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 1 ∈ ℝ+) |
24 | 3 | simplbda 503 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 1 ≤ 𝑥) |
25 | 4, 23, 24 | rpgecld 12566 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 𝑥 ∈ ℝ+) |
26 | 21, 25 | rerpdivcld 12558 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ) |
27 | | 2re 11803 |
. . . . . . 7
⊢ 2 ∈
ℝ |
28 | 27 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 2 ∈ ℝ) |
29 | 25 | relogcld 25379 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (log‘𝑥) ∈ ℝ) |
30 | 28, 29 | remulcld 10762 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ) |
31 | 26, 30 | resubcld 11159 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈
ℝ) |
32 | 31 | recnd 10760 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈
ℂ) |
33 | 25 | ex 416 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) → 𝑥
∈ ℝ+)) |
34 | 33 | ssrdv 3893 |
. . . 4
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ+) |
35 | | selberg 26297 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
36 | 35 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
37 | 34, 36 | o1res2 15023 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
38 | | fzfid 13445 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (1...(⌊‘𝑦)) ∈ Fin) |
39 | | elfznn 13040 |
. . . . . . . 8
⊢ (𝑛 ∈
(1...(⌊‘𝑦))
→ 𝑛 ∈
ℕ) |
40 | 39 | adantl 485 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℕ) |
41 | 40, 11 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑛) ∈
ℝ) |
42 | 40 | nnrpd 12525 |
. . . . . . . 8
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℝ+) |
43 | 42 | relogcld 25379 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (log‘𝑛) ∈
ℝ) |
44 | | simprl 771 |
. . . . . . . . . 10
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 𝑦 ∈ ℝ) |
45 | 44 | adantr 484 |
. . . . . . . . 9
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑦 ∈ ℝ) |
46 | 45, 40 | nndivred 11783 |
. . . . . . . 8
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑦 / 𝑛) ∈ ℝ) |
47 | | chpcl 25874 |
. . . . . . . 8
⊢ ((𝑦 / 𝑛) ∈ ℝ → (ψ‘(𝑦 / 𝑛)) ∈ ℝ) |
48 | 46, 47 | syl 17 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑦 / 𝑛)) ∈ ℝ) |
49 | 43, 48 | readdcld 10761 |
. . . . . 6
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))) ∈ ℝ) |
50 | 41, 49 | remulcld 10762 |
. . . . 5
⊢
(((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑦 / 𝑛)))) ∈
ℝ) |
51 | 38, 50 | fsumrecl 15197 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℝ) |
52 | 27 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 2 ∈ ℝ) |
53 | 22 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 1 ∈
ℝ+) |
54 | | simprr 773 |
. . . . . . 7
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 1 ≤ 𝑦) |
55 | 44, 53, 54 | rpgecld 12566 |
. . . . . 6
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → 𝑦 ∈ ℝ+) |
56 | 55 | relogcld 25379 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (log‘𝑦) ∈ ℝ) |
57 | 52, 56 | remulcld 10762 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (2 · (log‘𝑦)) ∈
ℝ) |
58 | 51, 57 | readdcld 10761 |
. . 3
⊢
((⊤ ∧ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦))) ∈
ℝ) |
59 | 31 | adantr 484 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈
ℝ) |
60 | 59 | recnd 10760 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈
ℂ) |
61 | 60 | abscld 14899 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
ℝ) |
62 | 26 | adantr 484 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ) |
63 | 30 | adantr 484 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑥)) ∈
ℝ) |
64 | 62, 63 | readdcld 10761 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥))) ∈ ℝ) |
65 | | fzfid 13445 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (1...(⌊‘𝑦)) ∈ Fin) |
66 | 39 | adantl 485 |
. . . . . . . 8
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℕ) |
67 | 66, 11 | syl 17 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑛) ∈
ℝ) |
68 | 66 | nnrpd 12525 |
. . . . . . . . 9
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℝ+) |
69 | 68 | relogcld 25379 |
. . . . . . . 8
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (log‘𝑛) ∈
ℝ) |
70 | | simprll 779 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ) |
71 | 70 | adantr 484 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑦 ∈ ℝ) |
72 | 71, 66 | nndivred 11783 |
. . . . . . . . 9
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑦 / 𝑛) ∈ ℝ) |
73 | 72, 47 | syl 17 |
. . . . . . . 8
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑦 / 𝑛)) ∈ ℝ) |
74 | 69, 73 | readdcld 10761 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))) ∈ ℝ) |
75 | 67, 74 | remulcld 10762 |
. . . . . 6
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑦 / 𝑛)))) ∈
ℝ) |
76 | 65, 75 | fsumrecl 15197 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℝ) |
77 | 27 | a1i 11 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℝ) |
78 | 25 | adantr 484 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ+) |
79 | 4 | adantr 484 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ) |
80 | | simprr 773 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦) |
81 | 79, 70, 80 | ltled 10879 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≤ 𝑦) |
82 | 70, 78, 81 | rpgecld 12566 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ+) |
83 | 82 | relogcld 25379 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑦) ∈ ℝ) |
84 | 77, 83 | remulcld 10762 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑦)) ∈
ℝ) |
85 | 76, 84 | readdcld 10761 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦))) ∈
ℝ) |
86 | 62 | recnd 10760 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℂ) |
87 | 63 | recnd 10760 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑥)) ∈
ℂ) |
88 | 86, 87 | abs2dif2d 14921 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤
((abs‘(Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) + (abs‘(2 · (log‘𝑥))))) |
89 | 21 | adantr 484 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ) |
90 | | vmage0 25871 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
91 | 10, 90 | syl 17 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑛)) |
92 | 10 | nnred 11744 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ) |
93 | 10 | nnge1d 11777 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑛) |
94 | 92, 93 | logge0d 25386 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(log‘𝑛)) |
95 | | chpge0 25876 |
. . . . . . . . . . . . 13
⊢ ((𝑥 / 𝑛) ∈ ℝ → 0 ≤
(ψ‘(𝑥 / 𝑛))) |
96 | 16, 95 | syl 17 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(ψ‘(𝑥 / 𝑛))) |
97 | 14, 18, 94, 96 | addge0d 11307 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((log‘𝑛) +
(ψ‘(𝑥 / 𝑛)))) |
98 | 12, 19, 91, 97 | mulge0d 11308 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛))))) |
99 | 8, 20, 98 | fsumge0 15256 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1[,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))))) |
100 | 99 | adantr 484 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))))) |
101 | 89, 78, 100 | divge0d 12567 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) |
102 | 62, 101 | absidd 14885 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) |
103 | 78 | relogcld 25379 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ∈ ℝ) |
104 | | 2rp 12490 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
105 | | rpge0 12498 |
. . . . . . . . 9
⊢ (2 ∈
ℝ+ → 0 ≤ 2) |
106 | 104, 105 | mp1i 13 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ 2) |
107 | 24 | adantr 484 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 1 ≤ 𝑥) |
108 | 79, 107 | logge0d 25386 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (log‘𝑥)) |
109 | 77, 103, 106, 108 | mulge0d 11308 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (2 · (log‘𝑥))) |
110 | 63, 109 | absidd 14885 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(2 ·
(log‘𝑥))) = (2
· (log‘𝑥))) |
111 | 102, 110 | oveq12d 7201 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) + (abs‘(2 · (log‘𝑥)))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥)))) |
112 | 88, 111 | breqtrd 5066 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥)))) |
113 | 22 | a1i 11 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 1 ∈
ℝ+) |
114 | 79 | adantr 484 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑥 ∈ ℝ) |
115 | 114, 66 | nndivred 11783 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑥 / 𝑛) ∈ ℝ) |
116 | 115, 17 | syl 17 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑥 / 𝑛)) ∈ ℝ) |
117 | 69, 116 | readdcld 10761 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))) ∈ ℝ) |
118 | 67, 117 | remulcld 10762 |
. . . . . . . . 9
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛)))) ∈
ℝ) |
119 | 65, 118 | fsumrecl 15197 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ) |
120 | 66, 90 | syl 17 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤
(Λ‘𝑛)) |
121 | 66 | nnred 11744 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℝ) |
122 | 66 | nnge1d 11777 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 1 ≤ 𝑛) |
123 | 121, 122 | logge0d 25386 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤
(log‘𝑛)) |
124 | 115, 95 | syl 17 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤
(ψ‘(𝑥 / 𝑛))) |
125 | 69, 116, 123, 124 | addge0d 11307 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤
((log‘𝑛) +
(ψ‘(𝑥 / 𝑛)))) |
126 | 67, 117, 120, 125 | mulge0d 11308 |
. . . . . . . . 9
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤
((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛))))) |
127 | | flword2 13287 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (⌊‘𝑦) ∈
(ℤ≥‘(⌊‘𝑥))) |
128 | 79, 70, 81, 127 | syl3anc 1372 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (⌊‘𝑦) ∈
(ℤ≥‘(⌊‘𝑥))) |
129 | | fzss2 13051 |
. . . . . . . . . 10
⊢
((⌊‘𝑦)
∈ (ℤ≥‘(⌊‘𝑥)) → (1...(⌊‘𝑥)) ⊆
(1...(⌊‘𝑦))) |
130 | 128, 129 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (1...(⌊‘𝑥)) ⊆
(1...(⌊‘𝑦))) |
131 | 65, 118, 126, 130 | fsumless 15257 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))))) |
132 | 81 | adantr 484 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑥 ≤ 𝑦) |
133 | 114, 71, 68, 132 | lediv1dd 12585 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑥 / 𝑛) ≤ (𝑦 / 𝑛)) |
134 | | chpwordi 25907 |
. . . . . . . . . . . 12
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ (𝑦 / 𝑛) ∈ ℝ ∧ (𝑥 / 𝑛) ≤ (𝑦 / 𝑛)) → (ψ‘(𝑥 / 𝑛)) ≤ (ψ‘(𝑦 / 𝑛))) |
135 | 115, 72, 133, 134 | syl3anc 1372 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑥 / 𝑛)) ≤ (ψ‘(𝑦 / 𝑛))) |
136 | 116, 73, 69, 135 | leadd2dd 11346 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))) ≤ ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) |
137 | 117, 74, 67, 120, 136 | lemul2ad 11671 |
. . . . . . . . 9
⊢
((((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛)))) ≤ ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))))) |
138 | 65, 118, 75, 137 | fsumle 15260 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))))) |
139 | 89, 119, 76, 131, 138 | letrd 10888 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))))) |
140 | 89, 76, 113, 79, 100, 139, 107 | lediv12ad 12586 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) / 1)) |
141 | 76 | recnd 10760 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℂ) |
142 | 141 | div1d 11499 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) / 1) = Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))))) |
143 | 140, 142 | breqtrd 5066 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))))) |
144 | 78, 82 | logled 25383 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 ≤ 𝑦 ↔ (log‘𝑥) ≤ (log‘𝑦))) |
145 | 81, 144 | mpbid 235 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ≤ (log‘𝑦)) |
146 | 103, 83, 77, 106, 145 | lemul2ad 11671 |
. . . . 5
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑥)) ≤ (2 ·
(log‘𝑦))) |
147 | 62, 63, 76, 84, 143, 146 | le2addd 11350 |
. . . 4
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦)))) |
148 | 61, 64, 85, 112, 147 | letrd 10888 |
. . 3
⊢
(((⊤ ∧ 𝑥
∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ (Σ𝑛 ∈
(1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦)))) |
149 | 6, 7, 32, 37, 58, 148 | o1bddrp 15002 |
. 2
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑥 ∈
(1[,)+∞)(abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐) |
150 | 149 | mptru 1549 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑥 ∈
(1[,)+∞)(abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐 |