| Step | Hyp | Ref
| Expression |
| 1 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 2 | | elicopnf 13485 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (𝑦 ∈
(1[,)+∞) ↔ (𝑦
∈ ℝ ∧ 1 ≤ 𝑦))) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ (1[,)+∞) ↔
(𝑦 ∈ ℝ ∧ 1
≤ 𝑦)) |
| 4 | 3 | simplbi 497 |
. . . . . 6
⊢ (𝑦 ∈ (1[,)+∞) →
𝑦 ∈
ℝ) |
| 5 | 4 | ssriv 3987 |
. . . . 5
⊢
(1[,)+∞) ⊆ ℝ |
| 6 | 5 | a1i 11 |
. . . 4
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ) |
| 7 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
| 8 | | fzfid 14014 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → (1...(⌊‘𝑦)) ∈ Fin) |
| 9 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(1...(⌊‘𝑦))
→ 𝑚 ∈
ℕ) |
| 10 | 9 | adantl 481 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 𝑚 ∈ ℕ) |
| 11 | | vmacl 27161 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑚) ∈
ℝ) |
| 13 | 10 | nnrpd 13075 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 𝑚 ∈ ℝ+) |
| 14 | 13 | relogcld 26665 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → (log‘𝑚) ∈
ℝ) |
| 15 | 12, 14 | remulcld 11291 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑚)
· (log‘𝑚))
∈ ℝ) |
| 16 | 8, 15 | fsumrecl 15770 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
| 17 | 4 | adantl 481 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → 𝑦 ∈ ℝ) |
| 18 | | chpcl 27167 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ →
(ψ‘𝑦) ∈
ℝ) |
| 19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → (ψ‘𝑦) ∈ ℝ) |
| 20 | | 1rp 13038 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ+ |
| 21 | 20 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → 1 ∈ ℝ+) |
| 22 | 3 | simprbi 496 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (1[,)+∞) → 1
≤ 𝑦) |
| 23 | 22 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → 1 ≤ 𝑦) |
| 24 | 17, 21, 23 | rpgecld 13116 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → 𝑦 ∈ ℝ+) |
| 25 | 24 | relogcld 26665 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → (log‘𝑦) ∈ ℝ) |
| 26 | 19, 25 | remulcld 11291 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℝ) |
| 27 | 16, 26 | resubcld 11691 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) ∈
ℝ) |
| 28 | 27, 24 | rerpdivcld 13108 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦) ∈ ℝ) |
| 29 | 28 | recnd 11289 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦) ∈ ℂ) |
| 30 | 24 | ex 412 |
. . . . . 6
⊢ (⊤
→ (𝑦 ∈
(1[,)+∞) → 𝑦
∈ ℝ+)) |
| 31 | 30 | ssrdv 3989 |
. . . . 5
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ+) |
| 32 | | selberg2lem 27594 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
↦ ((Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ∈ 𝑂(1) |
| 33 | 32 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑦 ∈
ℝ+ ↦ ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ∈ 𝑂(1)) |
| 34 | 31, 33 | o1res2 15599 |
. . . 4
⊢ (⊤
→ (𝑦 ∈
(1[,)+∞) ↦ ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ∈ 𝑂(1)) |
| 35 | | fzfid 14014 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
| 36 | | elfznn 13593 |
. . . . . . . . 9
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℕ) |
| 37 | 36 | adantl 481 |
. . . . . . . 8
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ) |
| 38 | 37, 11 | syl 17 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈
ℝ) |
| 39 | 37 | nnrpd 13075 |
. . . . . . . 8
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ+) |
| 40 | 39 | relogcld 26665 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈
ℝ) |
| 41 | 38, 40 | remulcld 11291 |
. . . . . 6
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑚)
· (log‘𝑚))
∈ ℝ) |
| 42 | 35, 41 | fsumrecl 15770 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
| 43 | | chpcl 27167 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
| 44 | 43 | ad2antrl 728 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → (ψ‘𝑥) ∈ ℝ) |
| 45 | | simprl 771 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
| 46 | 20 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → 1 ∈
ℝ+) |
| 47 | | simprr 773 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
| 48 | 45, 46, 47 | rpgecld 13116 |
. . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
| 49 | 48 | relogcld 26665 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ) |
| 50 | 44, 49 | remulcld 11291 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℝ) |
| 51 | 42, 50 | readdcld 11290 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))) ∈
ℝ) |
| 52 | 27 | adantr 480 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) ∈
ℝ) |
| 53 | 52 | recnd 11289 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) ∈
ℂ) |
| 54 | 24 | adantr 480 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ∈ ℝ+) |
| 55 | 54 | rpcnd 13079 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ∈ ℂ) |
| 56 | 54 | rpne0d 13082 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ≠ 0) |
| 57 | 53, 55, 56 | absdivd 15494 |
. . . . . 6
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / (abs‘𝑦))) |
| 58 | 17 | adantr 480 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ∈ ℝ) |
| 59 | 54 | rpge0d 13081 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ 𝑦) |
| 60 | 58, 59 | absidd 15461 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘𝑦) = 𝑦) |
| 61 | 60 | oveq2d 7447 |
. . . . . 6
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / (abs‘𝑦)) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦)) |
| 62 | 57, 61 | eqtrd 2777 |
. . . . 5
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦)) |
| 63 | 53 | abscld 15475 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ∈ ℝ) |
| 64 | 63, 54 | rerpdivcld 13108 |
. . . . . 6
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ∈ ℝ) |
| 65 | 42 | ad2ant2r 747 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
| 66 | | simprll 779 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑥 ∈ ℝ) |
| 67 | 66, 43 | syl 17 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (ψ‘𝑥) ∈ ℝ) |
| 68 | | simprr 773 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 < 𝑥) |
| 69 | 58, 66, 68 | ltled 11409 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ≤ 𝑥) |
| 70 | 66, 54, 69 | rpgecld 13116 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑥 ∈ ℝ+) |
| 71 | 70 | relogcld 26665 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (log‘𝑥) ∈ ℝ) |
| 72 | 67, 71 | remulcld 11291 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℝ) |
| 73 | 65, 72 | readdcld 11290 |
. . . . . 6
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))) ∈
ℝ) |
| 74 | 20 | a1i 11 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 1 ∈
ℝ+) |
| 75 | 53 | absge0d 15483 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))))) |
| 76 | 23 | adantr 480 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 1 ≤ 𝑦) |
| 77 | 74, 54, 63, 75, 76 | lediv2ad 13099 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ≤ ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 1)) |
| 78 | 63 | recnd 11289 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ∈ ℂ) |
| 79 | 78 | div1d 12035 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 1) = (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))))) |
| 80 | 77, 79 | breqtrd 5169 |
. . . . . 6
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ≤ (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))))) |
| 81 | 16 | adantr 480 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
| 82 | 58, 18 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (ψ‘𝑦) ∈ ℝ) |
| 83 | 54 | relogcld 26665 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (log‘𝑦) ∈ ℝ) |
| 84 | 82, 83 | remulcld 11291 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℝ) |
| 85 | 81, 84 | readdcld 11290 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦))) ∈
ℝ) |
| 86 | 81 | recnd 11289 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ∈
ℂ) |
| 87 | 26 | adantr 480 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℝ) |
| 88 | 87 | recnd 11289 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℂ) |
| 89 | 86, 88 | abs2dif2d 15497 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ≤ ((abs‘Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) + (abs‘((ψ‘𝑦) · (log‘𝑦))))) |
| 90 | | vmage0 27164 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 0 ≤
(Λ‘𝑚)) |
| 91 | 10, 90 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 0 ≤
(Λ‘𝑚)) |
| 92 | 10 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 𝑚 ∈ ℝ) |
| 93 | 10 | nnge1d 12314 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 1 ≤ 𝑚) |
| 94 | 92, 93 | logge0d 26672 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 0 ≤
(log‘𝑚)) |
| 95 | 12, 14, 91, 94 | mulge0d 11840 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 0 ≤
((Λ‘𝑚)
· (log‘𝑚))) |
| 96 | 8, 15, 95 | fsumge0 15831 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (1[,)+∞)) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) |
| 97 | 96 | adantr 480 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) |
| 98 | 81, 97 | absidd 15461 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) |
| 99 | | chpge0 27169 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 0 ≤
(ψ‘𝑦)) |
| 100 | 58, 99 | syl 17 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ (ψ‘𝑦)) |
| 101 | 58, 76 | logge0d 26672 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ (log‘𝑦)) |
| 102 | 82, 83, 100, 101 | mulge0d 11840 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ ((ψ‘𝑦) · (log‘𝑦))) |
| 103 | 87, 102 | absidd 15461 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((ψ‘𝑦) · (log‘𝑦))) = ((ψ‘𝑦) · (log‘𝑦))) |
| 104 | 98, 103 | oveq12d 7449 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) + (abs‘((ψ‘𝑦) · (log‘𝑦)))) = (Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦)))) |
| 105 | 89, 104 | breqtrd 5169 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦)))) |
| 106 | | fzfid 14014 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
| 107 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ) |
| 108 | 107, 11 | syl 17 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈
ℝ) |
| 109 | 107 | nnrpd 13075 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ+) |
| 110 | 109 | relogcld 26665 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈
ℝ) |
| 111 | 108, 110 | remulcld 11291 |
. . . . . . . . 9
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑚)
· (log‘𝑚))
∈ ℝ) |
| 112 | 107, 90 | syl 17 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑚)) |
| 113 | 107 | nnred 12281 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ) |
| 114 | 107 | nnge1d 12314 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑚) |
| 115 | 113, 114 | logge0d 26672 |
. . . . . . . . . 10
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤
(log‘𝑚)) |
| 116 | 108, 110,
112, 115 | mulge0d 11840 |
. . . . . . . . 9
⊢
((((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑚)
· (log‘𝑚))) |
| 117 | | flword2 13853 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑦))) |
| 118 | 58, 66, 69, 117 | syl3anc 1373 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑦))) |
| 119 | | fzss2 13604 |
. . . . . . . . . 10
⊢
((⌊‘𝑥)
∈ (ℤ≥‘(⌊‘𝑦)) → (1...(⌊‘𝑦)) ⊆
(1...(⌊‘𝑥))) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (1...(⌊‘𝑦)) ⊆
(1...(⌊‘𝑥))) |
| 121 | 106, 111,
116, 120 | fsumless 15832 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ≤ Σ𝑚 ∈
(1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚))) |
| 122 | | chpwordi 27200 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥) → (ψ‘𝑦) ≤ (ψ‘𝑥)) |
| 123 | 58, 66, 69, 122 | syl3anc 1373 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (ψ‘𝑦) ≤ (ψ‘𝑥)) |
| 124 | 54, 70 | logled 26669 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (𝑦 ≤ 𝑥 ↔ (log‘𝑦) ≤ (log‘𝑥))) |
| 125 | 69, 124 | mpbid 232 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (log‘𝑦) ≤ (log‘𝑥)) |
| 126 | 82, 67, 83, 71, 100, 101, 123, 125 | lemul12ad 12210 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ≤ ((ψ‘𝑥) · (log‘𝑥))) |
| 127 | 81, 84, 65, 72, 121, 126 | le2addd 11882 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦))) ≤ (Σ𝑚 ∈
(1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥)))) |
| 128 | 63, 85, 73, 105, 127 | letrd 11418 |
. . . . . 6
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥)))) |
| 129 | 64, 63, 73, 80, 128 | letrd 11418 |
. . . . 5
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥)))) |
| 130 | 62, 129 | eqbrtrd 5165 |
. . . 4
⊢
(((⊤ ∧ 𝑦
∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((Σ𝑚 ∈
(1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥)))) |
| 131 | 6, 7, 29, 34, 51, 130 | o1bddrp 15578 |
. . 3
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) |
| 132 | 131 | mptru 1547 |
. 2
⊢
∃𝑐 ∈
ℝ+ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐 |
| 133 | | simpl 482 |
. . . 4
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) → 𝑐 ∈ ℝ+) |
| 134 | | simpr 484 |
. . . 4
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) → ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) |
| 135 | 133, 134 | selberg3lem1 27601 |
. . 3
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ ((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)) |
| 136 | 135 | rexlimiva 3147 |
. 2
⊢
(∃𝑐 ∈
ℝ+ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦ ((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)) |
| 137 | 132, 136 | ax-mp 5 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((2 / (log‘𝑥))
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1) |