Proof of Theorem selberg4lem1
| Step | Hyp | Ref
| Expression |
| 1 | | 2cnd 12344 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈
ℂ) |
| 2 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(1...(⌊‘𝑥))
∈ Fin) |
| 3 | | elfznn 13593 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 4 | 3 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 5 | | vmacl 27161 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
| 7 | 6, 4 | nndivred 12320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
| 8 | | elioore 13417 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
| 9 | 8 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ) |
| 10 | | 1rp 13038 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ+ |
| 11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ+) |
| 12 | | 1red 11262 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ) |
| 13 | | eliooord 13446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
| 15 | 14 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥) |
| 16 | 12, 9, 15 | ltled 11409 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥) |
| 17 | 9, 11, 16 | rpgecld 13116 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ+) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
| 19 | 4 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
| 20 | 18, 19 | rpdivcld 13094 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
| 21 | 20 | relogcld 26665 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℝ) |
| 22 | 7, 21 | remulcld 11291 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
| 23 | 2, 22 | fsumrecl 15770 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ) |
| 24 | 9, 15 | rplogcld 26671 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ+) |
| 25 | 23, 24 | rerpdivcld 13108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℝ) |
| 26 | 25 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ) |
| 27 | 17 | relogcld 26665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ) |
| 28 | 27 | rehalfcld 12513 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) / 2) ∈
ℝ) |
| 29 | 28 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) / 2) ∈
ℂ) |
| 30 | 1, 26, 29 | subdid 11719 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (2 · ((log‘𝑥) / 2)))) |
| 31 | 27 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℂ) |
| 32 | | 2ne0 12370 |
. . . . . . . 8
⊢ 2 ≠
0 |
| 33 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ≠
0) |
| 34 | 31, 1, 33 | divcan2d 12045 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
((log‘𝑥) / 2)) =
(log‘𝑥)) |
| 35 | 34 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (2 · ((log‘𝑥) / 2))) = ((2 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) |
| 36 | 30, 35 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) |
| 37 | 36 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (2 ·
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) = (𝑥 ∈ (1(,)+∞) ↦ ((2 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)))) |
| 38 | | 2re 12340 |
. . . . 5
⊢ 2 ∈
ℝ |
| 39 | 38 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈
ℝ) |
| 40 | 25, 28 | resubcld 11691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ) |
| 41 | | ioossre 13448 |
. . . . . 6
⊢
(1(,)+∞) ⊆ ℝ |
| 42 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 43 | | o1const 15656 |
. . . . . 6
⊢
(((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1)) |
| 44 | 41, 42, 43 | mp2an 692 |
. . . . 5
⊢ (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1) |
| 45 | 44 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈
𝑂(1)) |
| 46 | | vmalogdivsum2 27582 |
. . . . 5
⊢ (𝑥 ∈ (1(,)+∞) ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) |
| 47 | 46 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1)) |
| 48 | 39, 40, 45, 47 | o1mul2 15661 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (2 ·
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈
𝑂(1)) |
| 49 | 37, 48 | eqeltrrd 2842 |
. 2
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((2 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1)) |
| 50 | | fzfid 14014 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin) |
| 51 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
| 52 | 51 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ∈
ℕ) |
| 53 | | vmacl 27161 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
| 54 | 52, 53 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(Λ‘𝑚) ∈
ℝ) |
| 55 | 52 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ∈
ℝ+) |
| 56 | 55 | relogcld 26665 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(log‘𝑚) ∈
ℝ) |
| 57 | 9 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
| 58 | 57, 4 | nndivred 12320 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → (𝑥 / 𝑛) ∈ ℝ) |
| 60 | 59, 52 | nndivred 12320 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ) |
| 61 | | chpcl 27167 |
. . . . . . . . . . . 12
⊢ (((𝑥 / 𝑛) / 𝑚) ∈ ℝ → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ) |
| 63 | 56, 62 | readdcld 11290 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((log‘𝑚) +
(ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℝ) |
| 64 | 54, 63 | remulcld 11291 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((Λ‘𝑚)
· ((log‘𝑚) +
(ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ) |
| 65 | 50, 64 | fsumrecl 15770 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ) |
| 66 | 6, 65 | remulcld 11291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ) |
| 67 | 2, 66 | fsumrecl 15770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ) |
| 68 | 17, 24 | rpmulcld 13093 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ+) |
| 69 | 67, 68 | rerpdivcld 13108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
| 70 | 69, 27 | resubcld 11691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) ∈ ℝ) |
| 71 | 70 | recnd 11289 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) ∈ ℂ) |
| 72 | 23 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ) |
| 73 | 24 | rpne0d 13082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ≠
0) |
| 74 | 72, 31, 73 | divcld 12043 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ) |
| 75 | 1, 74 | mulcld 11281 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) ∈ ℂ) |
| 76 | 75, 31 | subcld 11620 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)) ∈ ℂ) |
| 77 | 69 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) ∈ ℂ) |
| 78 | 77, 75, 31 | nnncan2d 11655 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))) |
| 79 | 67 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ) |
| 80 | 9 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℂ) |
| 81 | 17 | rpne0d 13082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0) |
| 82 | 79, 80, 31, 81, 73 | divdiv1d 12074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥)))) |
| 83 | 1, 72, 31, 73 | divassd 12078 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))) |
| 84 | 82, 83 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) − ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))) |
| 85 | 67, 17 | rerpdivcld 13108 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℝ) |
| 86 | 85 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℂ) |
| 87 | 1, 72 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) |
| 88 | 86, 87, 31, 73 | divsubdird 12082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) / (log‘𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) − ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))) |
| 89 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ≠
0) |
| 90 | 66, 57, 89 | redivcld 12095 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℝ) |
| 91 | 90 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℂ) |
| 92 | 38 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℝ) |
| 93 | 92, 22 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℝ) |
| 94 | 93 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) |
| 95 | 2, 91, 94 | fsumsub 15824 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))(2 ·
(((Λ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛)))))) |
| 96 | 6 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
| 97 | 65, 57, 89 | redivcld 12095 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) ∈ ℝ) |
| 98 | 97 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) ∈ ℂ) |
| 99 | | 2cnd 12344 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) |
| 100 | 21 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℂ) |
| 101 | 4 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
| 102 | 4 | nnne0d 12316 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
| 103 | 100, 101,
102 | divcld 12043 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛)) / 𝑛) ∈ ℂ) |
| 104 | 99, 103 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) ∈ ℂ) |
| 105 | 96, 98, 104 | subdid 11719 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥)) − ((Λ‘𝑛) · (2 ·
((log‘(𝑥 / 𝑛)) / 𝑛))))) |
| 106 | 65 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ) |
| 107 | 80 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
| 108 | 96, 106, 107, 89 | divassd 12078 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) = ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥))) |
| 109 | 96, 101, 100, 102 | div32d 12066 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) ·
(log‘(𝑥 / 𝑛))) = ((Λ‘𝑛) · ((log‘(𝑥 / 𝑛)) / 𝑛))) |
| 110 | 109 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (2 · ((Λ‘𝑛) · ((log‘(𝑥 / 𝑛)) / 𝑛)))) |
| 111 | 99, 96, 103 | mul12d 11470 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · ((Λ‘𝑛) · ((log‘(𝑥 / 𝑛)) / 𝑛))) = ((Λ‘𝑛) · (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) |
| 112 | 110, 111 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = ((Λ‘𝑛) · (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) |
| 113 | 108, 112 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥)) − ((Λ‘𝑛) · (2 ·
((log‘(𝑥 / 𝑛)) / 𝑛))))) |
| 114 | 105, 113 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) = ((((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) |
| 115 | 114 | sumeq2dv 15738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) |
| 116 | 66 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ) |
| 117 | 2, 80, 116, 81 | fsumdivc 15822 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥)) |
| 118 | 22 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℂ) |
| 119 | 2, 1, 118 | fsummulc2 15820 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 ·
(((Λ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛))))) |
| 120 | 117, 119 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))(2 ·
(((Λ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛)))))) |
| 121 | 95, 115, 120 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) |
| 122 | 121 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) |
| 123 | 88, 122 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) − ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) |
| 124 | 78, 84, 123 | 3eqtr2d 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) |
| 125 | 124 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)))) |
| 126 | | 1red 11262 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
| 127 | | selberg4lem1.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
| 128 | 127 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℝ+) |
| 129 | 128 | rpred 13077 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℝ) |
| 130 | 2, 7 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
| 131 | 130, 24 | rerpdivcld 13108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ) |
| 132 | 127 | rpcnd 13079 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 133 | | o1const 15656 |
. . . . . . 7
⊢
(((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
| 134 | 41, 132, 133 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
| 135 | | 1cnd 11256 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
| 136 | | o1const 15656 |
. . . . . . . 8
⊢
(((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1)) |
| 137 | 41, 135, 136 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈
𝑂(1)) |
| 138 | 131 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ) |
| 139 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℂ) |
| 140 | 130 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
| 141 | 140, 31, 31, 73 | divsubdird 12082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥)))) |
| 142 | 140, 31 | subcld 11620 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
| 143 | 142, 31, 73 | divrecd 12046 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) |
| 144 | 31, 73 | dividd 12041 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) /
(log‘𝑥)) =
1) |
| 145 | 144 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) |
| 146 | 141, 143,
145 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) |
| 147 | 146 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))) |
| 148 | 130, 27 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ) |
| 149 | 12, 24 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 /
(log‘𝑥)) ∈
ℝ) |
| 150 | 17 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈
ℝ+)) |
| 151 | 150 | ssrdv 3989 |
. . . . . . . . . . 11
⊢ (𝜑 → (1(,)+∞) ⊆
ℝ+) |
| 152 | | vmadivsum 27526 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
| 153 | 152 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
| 154 | 151, 153 | o1res2 15599 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
| 155 | | divlogrlim 26677 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 |
| 156 | | rlimo1 15653 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
| 157 | 155, 156 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
| 158 | 148, 149,
154, 157 | o1mul2 15661 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈
𝑂(1)) |
| 159 | 147, 158 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈
𝑂(1)) |
| 160 | 138, 139,
159 | o1dif 15666 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1))) |
| 161 | 137, 160 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1)) |
| 162 | 129, 131,
134, 161 | o1mul2 15661 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (𝐴 · (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) ∈ 𝑂(1)) |
| 163 | 129, 131 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ ℝ) |
| 164 | 21, 4 | nndivred 12320 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛)) / 𝑛) ∈ ℝ) |
| 165 | 92, 164 | remulcld 11291 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) ∈ ℝ) |
| 166 | 97, 165 | resubcld 11691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) ∈ ℝ) |
| 167 | 6, 166 | remulcld 11291 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℝ) |
| 168 | 2, 167 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℝ) |
| 169 | 168, 24 | rerpdivcld 13108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)) ∈ ℝ) |
| 170 | 169 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)) ∈ ℂ) |
| 171 | 168 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℂ) |
| 172 | 171 | abscld 15475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ∈ ℝ) |
| 173 | 129, 130 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
| 174 | 98, 104 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) ∈ ℂ) |
| 175 | 96, 174 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℂ) |
| 176 | 175 | abscld 15475 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ∈ ℝ) |
| 177 | 2, 176 | fsumrecl 15770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ∈ ℝ) |
| 178 | 167 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℂ) |
| 179 | 2, 178 | fsumabs 15837 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))))) |
| 180 | 129 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈
ℝ) |
| 181 | 180, 7 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 ·
((Λ‘𝑛) / 𝑛)) ∈
ℝ) |
| 182 | 174 | abscld 15475 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℝ) |
| 183 | 180, 4 | nndivred 12320 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 / 𝑛) ∈
ℝ) |
| 184 | | vmage0 27164 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
| 185 | 4, 184 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (Λ‘𝑛)) |
| 186 | 106, 107,
101, 89, 102 | divdiv2d 12075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) · 𝑛) / 𝑥)) |
| 187 | 106, 101,
107, 89 | div23d 12080 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) · 𝑛) / 𝑥) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛)) |
| 188 | 186, 187 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛)) |
| 189 | 99, 103, 101 | mulassd 11284 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑛) · 𝑛))) |
| 190 | 100, 101,
102 | divcan1d 12044 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑥 /
𝑛)) / 𝑛) · 𝑛) = (log‘(𝑥 / 𝑛))) |
| 191 | 190 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((log‘(𝑥 / 𝑛)) / 𝑛) · 𝑛)) = (2 · (log‘(𝑥 / 𝑛)))) |
| 192 | 189, 191 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (log‘(𝑥 / 𝑛))) = ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛)) |
| 193 | 188, 192 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛)))) = (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛) − ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛))) |
| 194 | 98, 104, 101 | subdird 11720 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛) = (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛) − ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛))) |
| 195 | 193, 194 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛)))) = (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛)) |
| 196 | 195 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) = (abs‘(((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛))) |
| 197 | 174, 101 | absmuld 15493 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛)) = ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · (abs‘𝑛))) |
| 198 | 4 | nnred 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
| 199 | 19 | rpge0d 13081 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ 𝑛) |
| 200 | 198, 199 | absidd 15461 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘𝑛) =
𝑛) |
| 201 | 200 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · (abs‘𝑛)) = ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛)) |
| 202 | 196, 197,
201 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) = ((abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛)) |
| 203 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 𝑚 → (Λ‘𝑖) = (Λ‘𝑚)) |
| 204 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 𝑚 → (log‘𝑖) = (log‘𝑚)) |
| 205 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = 𝑚 → (𝑦 / 𝑖) = (𝑦 / 𝑚)) |
| 206 | 205 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 𝑚 → (ψ‘(𝑦 / 𝑖)) = (ψ‘(𝑦 / 𝑚))) |
| 207 | 204, 206 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = 𝑚 → ((log‘𝑖) + (ψ‘(𝑦 / 𝑖))) = ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))) |
| 208 | 203, 207 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑚 → ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) = ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚))))) |
| 209 | 208 | cbvsumv 15732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Σ𝑖 ∈
(1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))) |
| 210 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛))) |
| 211 | 210 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛)))) |
| 212 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = (𝑥 / 𝑛) → (ψ‘(𝑦 / 𝑚)) = (ψ‘((𝑥 / 𝑛) / 𝑚))) |
| 213 | 212 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝑥 / 𝑛) → ((log‘𝑚) + (ψ‘(𝑦 / 𝑚))) = ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) |
| 214 | 213 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑥 / 𝑛) → ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))) = ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
| 215 | 214 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 = (𝑥 / 𝑛) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) →
((Λ‘𝑚)
· ((log‘𝑚) +
(ψ‘(𝑦 / 𝑚)))) = ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
| 216 | 211, 215 | sumeq12dv 15742 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
| 217 | 209, 216 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
| 218 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑥 / 𝑛) → 𝑦 = (𝑥 / 𝑛)) |
| 219 | 217, 218 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 / 𝑛) → (Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛))) |
| 220 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛))) |
| 221 | 220 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 / 𝑛) → (2 · (log‘𝑦)) = (2 ·
(log‘(𝑥 / 𝑛)))) |
| 222 | 219, 221 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑥 / 𝑛) → ((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦))) = ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) |
| 223 | 222 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑥 / 𝑛) → (abs‘((Σ𝑖 ∈
(1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) = (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛)))))) |
| 224 | 223 | breq1d 5153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 / 𝑛) → ((abs‘((Σ𝑖 ∈
(1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴 ↔ (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) ≤ 𝐴)) |
| 225 | | selberg4lem1.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴) |
| 226 | 225 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴) |
| 227 | 101 | mullidd 11279 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) =
𝑛) |
| 228 | | fznnfl 13902 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
| 229 | 9, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
| 230 | 229 | simplbda 499 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≤ 𝑥) |
| 231 | 227, 230 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) ≤
𝑥) |
| 232 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
| 233 | 232, 57, 19 | lemuldivd 13126 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 · 𝑛) ≤
𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
| 234 | 231, 233 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ (𝑥 / 𝑛)) |
| 235 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
| 236 | | elicopnf 13485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔
((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))) |
| 237 | 235, 236 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))) |
| 238 | 58, 234, 237 | sylanbrc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
(1[,)+∞)) |
| 239 | 224, 226,
238 | rspcdva 3623 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) ≤ 𝐴) |
| 240 | 202, 239 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛) ≤ 𝐴) |
| 241 | 182, 180,
19 | lemuldivd 13126 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛) ≤ 𝐴 ↔ (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ≤ (𝐴 / 𝑛))) |
| 242 | 240, 241 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ≤ (𝐴 / 𝑛)) |
| 243 | 182, 183,
6, 185, 242 | lemul2ad 12208 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ ((Λ‘𝑛) · (𝐴 / 𝑛))) |
| 244 | 96, 174 | absmuld 15493 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) = ((abs‘(Λ‘𝑛)) ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))))) |
| 245 | 6, 185 | absidd 15461 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Λ‘𝑛)) = (Λ‘𝑛)) |
| 246 | 245 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(Λ‘𝑛)) · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) = ((Λ‘𝑛) · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))))) |
| 247 | 244, 246 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) = ((Λ‘𝑛) · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))))) |
| 248 | 132 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈
ℂ) |
| 249 | 248, 96, 101, 102 | div12d 12079 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 ·
((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) · (𝐴 / 𝑛))) |
| 250 | 243, 247,
249 | 3brtr4d 5175 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ (𝐴 · ((Λ‘𝑛) / 𝑛))) |
| 251 | 2, 176, 181, 250 | fsumle 15835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(𝐴 · ((Λ‘𝑛) / 𝑛))) |
| 252 | 132 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℂ) |
| 253 | 7 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℂ) |
| 254 | 2, 252, 253 | fsummulc2 15820 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝐴 · ((Λ‘𝑛) / 𝑛))) |
| 255 | 251, 254 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛))) |
| 256 | 172, 177,
173, 179, 255 | letrd 11418 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛))) |
| 257 | 172, 173,
24, 256 | lediv1dd 13135 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥)) ≤ ((𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) / (log‘𝑥))) |
| 258 | 252, 140,
31, 73 | divassd 12078 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((𝐴 · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) / (log‘𝑥)) = (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) |
| 259 | 257, 258 | breqtrd 5169 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥)) ≤ (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) |
| 260 | 171, 31, 73 | absdivd 15494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (abs‘(log‘𝑥)))) |
| 261 | 24 | rpge0d 13081 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
(log‘𝑥)) |
| 262 | 27, 261 | absidd 15461 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(log‘𝑥)) =
(log‘𝑥)) |
| 263 | 262 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (abs‘(log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥))) |
| 264 | 260, 263 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥))) |
| 265 | 128 | rpge0d 13081 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 𝐴) |
| 266 | 6, 19, 185 | divge0d 13117 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((Λ‘𝑛) / 𝑛)) |
| 267 | 2, 7, 266 | fsumge0 15831 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) |
| 268 | 130, 24, 267 | divge0d 13117 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) |
| 269 | 129, 131,
265, 268 | mulge0d 11840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝐴 · (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) |
| 270 | 163, 269 | absidd 15461 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(𝐴 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) = (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) |
| 271 | 259, 264,
270 | 3brtr4d 5175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) ≤ (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))))) |
| 272 | 271 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) ≤ (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))))) |
| 273 | 126, 162,
163, 170, 272 | o1le 15689 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1)) |
| 274 | 125, 273 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)))) ∈ 𝑂(1)) |
| 275 | 71, 76, 274 | o1dif 15666 |
. 2
⊢ (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
((2 · (Σ𝑛
∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1))) |
| 276 | 49, 275 | mpbird 257 |
1
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1)) |