| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2cn 12341 | . . . . . 6
⊢ 2 ∈
ℂ | 
| 2 | 1 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) | 
| 3 |  | fzfid 14014 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) | 
| 4 |  | elfznn 13593 | . . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) | 
| 5 | 4 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) | 
| 6 |  | mucl 27184 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) | 
| 7 | 5, 6 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) | 
| 8 | 7 | zred 12722 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℝ) | 
| 9 | 8, 5 | nndivred 12320 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℝ) | 
| 10 | 9 | recnd 11289 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) | 
| 11 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 12 | 4 | nnrpd 13075 | . . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) | 
| 13 |  | rpdivcl 13060 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 14 | 11, 12, 13 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) | 
| 15 | 14 | relogcld 26665 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℝ) | 
| 16 | 15 | recnd 11289 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℂ) | 
| 17 | 16 | sqcld 14184 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛))↑2) ∈
ℂ) | 
| 18 | 17 | halfcld 12511 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑥 /
𝑛))↑2) / 2) ∈
ℂ) | 
| 19 | 10, 18 | mulcld 11281 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
(((log‘(𝑥 / 𝑛))↑2) / 2)) ∈
ℂ) | 
| 20 | 3, 19 | fsumcl 15769 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) ∈
ℂ) | 
| 21 |  | relogcl 26617 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) | 
| 22 | 21 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) | 
| 23 | 22 | recnd 11289 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) | 
| 24 | 2, 20, 23 | subdid 11719 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥))) = ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) − (2 ·
(log‘𝑥)))) | 
| 25 | 3, 2, 19 | fsummulc2 15820 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 ·
(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)))) | 
| 26 | 1 | a1i 11 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) | 
| 27 | 26, 10, 18 | mul12d 11470 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) = (((μ‘𝑛) / 𝑛) · (2 · (((log‘(𝑥 / 𝑛))↑2) / 2)))) | 
| 28 |  | 2ne0 12370 | . . . . . . . . . . 11
⊢ 2 ≠
0 | 
| 29 | 28 | a1i 11 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ≠ 0) | 
| 30 | 17, 26, 29 | divcan2d 12045 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((log‘(𝑥 / 𝑛))↑2) / 2)) = ((log‘(𝑥 / 𝑛))↑2)) | 
| 31 | 30 | oveq2d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · (2 ·
(((log‘(𝑥 / 𝑛))↑2) / 2))) =
(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2))) | 
| 32 | 27, 31 | eqtrd 2777 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) = (((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2))) | 
| 33 | 32 | sumeq2dv 15738 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(2
· (((μ‘𝑛) /
𝑛) ·
(((log‘(𝑥 / 𝑛))↑2) / 2))) = Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2))) | 
| 34 | 25, 33 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2))) | 
| 35 | 34 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) − (2 ·
(log‘𝑥))) =
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥)))) | 
| 36 | 24, 35 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥)))) | 
| 37 | 36 | mpteq2dva 5242 | . 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))))) | 
| 38 | 20, 23 | subcld 11620 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥)) ∈
ℂ) | 
| 39 |  | rpssre 13042 | . . . . 5
⊢
ℝ+ ⊆ ℝ | 
| 40 |  | o1const 15656 | . . . . 5
⊢
((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 2) ∈ 𝑂(1)) | 
| 41 | 39, 1, 40 | mp2an 692 | . . . 4
⊢ (𝑥 ∈ ℝ+
↦ 2) ∈ 𝑂(1) | 
| 42 | 41 | a1i 11 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈
𝑂(1)) | 
| 43 |  | emre 27049 | . . . . . . . . . . . . 13
⊢ γ
∈ ℝ | 
| 44 | 43 | recni 11275 | . . . . . . . . . . . 12
⊢ γ
∈ ℂ | 
| 45 |  | mulcl 11239 | . . . . . . . . . . . 12
⊢ ((γ
∈ ℂ ∧ (log‘(𝑥 / 𝑛)) ∈ ℂ) → (γ ·
(log‘(𝑥 / 𝑛))) ∈
ℂ) | 
| 46 | 44, 16, 45 | sylancr 587 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ) | 
| 47 |  | mulog2sumlem.1 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) | 
| 48 |  | rlimcl 15539 | . . . . . . . . . . . . 13
⊢ (𝐹 ⇝𝑟
𝐿 → 𝐿 ∈ ℂ) | 
| 49 | 47, 48 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ ℂ) | 
| 50 | 49 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐿 ∈
ℂ) | 
| 51 | 46, 50 | subcld 11620 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ) | 
| 52 | 18, 51 | addcld 11280 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((log‘(𝑥 /
𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ) | 
| 53 | 10, 52 | mulcld 11281 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ
· (log‘(𝑥 /
𝑛))) − 𝐿))) ∈
ℂ) | 
| 54 | 3, 53 | fsumcl 15769 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℂ) | 
| 55 | 10, 51 | mulcld 11281 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · ((γ
· (log‘(𝑥 /
𝑛))) − 𝐿)) ∈
ℂ) | 
| 56 | 3, 55 | fsumcl 15769 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ) | 
| 57 | 54, 23, 56 | sub32d 11652 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥))) | 
| 58 | 3, 53, 55 | fsumsub 15824 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)))) | 
| 59 | 10, 52, 51 | subdid 11719 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
(((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ
· (log‘(𝑥 /
𝑛))) − 𝐿)) − ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = ((((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)))) | 
| 60 | 18, 51 | pncand 11621 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((((log‘(𝑥 /
𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) − ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)) = (((log‘(𝑥 / 𝑛))↑2) / 2)) | 
| 61 | 60 | oveq2d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
(((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ
· (log‘(𝑥 /
𝑛))) − 𝐿)) − ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = (((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) | 
| 62 | 59, 61 | eqtr3d 2779 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((μ‘𝑛) /
𝑛) ·
((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ
· (log‘(𝑥 /
𝑛))) − 𝐿))) − (((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = (((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) | 
| 63 | 62 | sumeq2dv 15738 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) | 
| 64 | 58, 63 | eqtr3d 2779 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2))) | 
| 65 | 64 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥))) | 
| 66 | 57, 65 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥))) | 
| 67 | 66 | mpteq2dva 5242 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥)))) | 
| 68 | 54, 23 | subcld 11620 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥)) ∈ ℂ) | 
| 69 |  | logdivsum.1 | . . . . . 6
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦
(Σ𝑖 ∈
(1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) | 
| 70 |  | eqid 2737 | . . . . . 6
⊢
((((log‘(𝑥 /
𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)) | 
| 71 |  | eqid 2737 | . . . . . 6
⊢ (((1 / 2)
+ (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) | 
| 72 | 69, 47, 70, 71 | mulog2sumlem2 27579 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥))) ∈ 𝑂(1)) | 
| 73 | 44 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → γ
∈ ℂ) | 
| 74 | 10, 16 | mulcld 11281 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℂ) | 
| 75 | 3, 73, 74 | fsummulc2 15820 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (γ
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(γ ·
(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) | 
| 76 | 49 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿 ∈
ℂ) | 
| 77 | 3, 76, 10 | fsummulc1 15821 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · 𝐿) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝐿)) | 
| 78 | 75, 77 | oveq12d 7449 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((γ
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · 𝐿)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(γ ·
(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝐿))) | 
| 79 |  | mulcl 11239 | . . . . . . . . . 10
⊢ ((γ
∈ ℂ ∧ (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ) → (γ ·
(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) | 
| 80 | 44, 74, 79 | sylancr 587 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (γ · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) | 
| 81 | 10, 50 | mulcld 11281 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · 𝐿) ∈
ℂ) | 
| 82 | 3, 80, 81 | fsumsub 15824 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((γ · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · 𝐿)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(γ ·
(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝐿))) | 
| 83 | 44 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ γ ∈ ℂ) | 
| 84 | 83, 10, 16 | mul12d 11470 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (γ · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (((μ‘𝑛) / 𝑛) · (γ ·
(log‘(𝑥 / 𝑛))))) | 
| 85 | 84 | oveq1d 7446 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((γ · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · 𝐿)) = ((((μ‘𝑛) / 𝑛) · (γ ·
(log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · 𝐿))) | 
| 86 | 10, 46, 50 | subdid 11719 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · ((γ
· (log‘(𝑥 /
𝑛))) − 𝐿)) = ((((μ‘𝑛) / 𝑛) · (γ ·
(log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · 𝐿))) | 
| 87 | 85, 86 | eqtr4d 2780 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((γ · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · 𝐿)) = (((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) | 
| 88 | 87 | sumeq2dv 15738 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((γ · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · 𝐿)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) | 
| 89 | 78, 82, 88 | 3eqtr2d 2783 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((γ
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · 𝐿)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) | 
| 90 | 89 | mpteq2dva 5242 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((γ
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · 𝐿))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)))) | 
| 91 | 3, 74 | fsumcl 15769 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ) | 
| 92 |  | mulcl 11239 | . . . . . . . 8
⊢ ((γ
∈ ℂ ∧ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ) → (γ ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) | 
| 93 | 44, 91, 92 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (γ
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) | 
| 94 | 3, 10 | fsumcl 15769 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) | 
| 95 | 94, 76 | mulcld 11281 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · 𝐿) ∈ ℂ) | 
| 96 | 44 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → γ ∈
ℂ) | 
| 97 |  | o1const 15656 | . . . . . . . . 9
⊢
((ℝ+ ⊆ ℝ ∧ γ ∈ ℂ)
→ (𝑥 ∈
ℝ+ ↦ γ) ∈ 𝑂(1)) | 
| 98 | 39, 96, 97 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ γ)
∈ 𝑂(1)) | 
| 99 |  | mulogsum 27576 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ 𝑂(1) | 
| 100 | 99 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ 𝑂(1)) | 
| 101 | 73, 91, 98, 100 | o1mul2 15661 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (γ
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1)) | 
| 102 |  | mudivsum 27574 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1) | 
| 103 | 102 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)) | 
| 104 |  | o1const 15656 | . . . . . . . . 9
⊢
((ℝ+ ⊆ ℝ ∧ 𝐿 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 𝐿) ∈
𝑂(1)) | 
| 105 | 39, 49, 104 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 𝐿) ∈
𝑂(1)) | 
| 106 | 94, 76, 103, 105 | o1mul2 15661 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · 𝐿)) ∈ 𝑂(1)) | 
| 107 | 93, 95, 101, 106 | o1sub2 15662 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((γ
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · 𝐿))) ∈ 𝑂(1)) | 
| 108 | 90, 107 | eqeltrrd 2842 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) ∈ 𝑂(1)) | 
| 109 | 68, 56, 72, 108 | o1sub2 15662 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)))) ∈ 𝑂(1)) | 
| 110 | 67, 109 | eqeltrrd 2842 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥))) ∈
𝑂(1)) | 
| 111 | 2, 38, 42, 110 | o1mul2 15661 | . 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) / 2)) − (log‘𝑥)))) ∈
𝑂(1)) | 
| 112 | 37, 111 | eqeltrrd 2842 | 1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥)))) ∈
𝑂(1)) |