Proof of Theorem selberglem1
Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
2 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
3 | 2 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
4 | | mucl 24667 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) |
6 | 5 | zred 11358 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℝ) |
7 | 6, 3 | nndivred 10946 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℝ) |
8 | 7 | recnd 9947 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) |
9 | 2 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
10 | | rpdivcl 11732 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
11 | 9, 10 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
12 | | relogcl 24126 |
. . . . . . . . . 10
⊢ ((𝑥 / 𝑛) ∈ ℝ+ →
(log‘(𝑥 / 𝑛)) ∈
ℝ) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℝ) |
14 | 13 | recnd 9947 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℂ) |
15 | 14 | sqcld 12868 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛))↑2) ∈
ℂ) |
16 | 8, 15 | mulcld 9939 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
((log‘(𝑥 / 𝑛))↑2)) ∈
ℂ) |
17 | 1, 16 | fsumcl 14311 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) ∈ ℂ) |
18 | | 2cn 10968 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) |
20 | 19, 14 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (log‘(𝑥 / 𝑛))) ∈ ℂ) |
21 | 19, 20 | subcld 10271 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℂ) |
22 | 8, 21 | mulcld 9939 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈
ℂ) |
23 | 1, 22 | fsumcl 14311 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈
ℂ) |
24 | | relogcl 24126 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
25 | 24 | recnd 9947 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
26 | | mulcl 9899 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 ·
(log‘𝑥)) ∈
ℂ) |
27 | 18, 25, 26 | sylancr 694 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (2 · (log‘𝑥)) ∈ ℂ) |
28 | 17, 23, 27 | addsubd 10292 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) − (2 ·
(log‘𝑥))) =
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) +
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
29 | | selberglem1.t |
. . . . . . . . 9
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛) |
30 | 29 | oveq2i 6560 |
. . . . . . . 8
⊢
((μ‘𝑛)
· 𝑇) =
((μ‘𝑛) ·
((((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) / 𝑛)) |
31 | 5 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) |
32 | 15, 21 | addcld 9938 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑥 /
𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈
ℂ) |
33 | 3 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
34 | 33 | rpcnne0d 11757 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
35 | | divass 10582 |
. . . . . . . . . . 11
⊢
(((μ‘𝑛)
∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) →
(((μ‘𝑛) ·
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛)))))) / 𝑛) = ((μ‘𝑛) · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛))) |
36 | | div23 10583 |
. . . . . . . . . . 11
⊢
(((μ‘𝑛)
∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) →
(((μ‘𝑛) ·
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛)))))) / 𝑛) = (((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
37 | 35, 36 | eqtr3d 2646 |
. . . . . . . . . 10
⊢
(((μ‘𝑛)
∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) →
((μ‘𝑛) ·
((((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) / 𝑛)) = (((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
38 | 31, 32, 34, 37 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛)
· ((((log‘(𝑥 /
𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) / 𝑛)) = (((μ‘𝑛) / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
39 | 8, 15, 21 | adddid 9943 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛)))))) =
((((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + (((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
40 | 38, 39 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛)
· ((((log‘(𝑥 /
𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) / 𝑛)) = ((((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + (((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
41 | 30, 40 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛)
· 𝑇) =
((((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + (((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
42 | 41 | sumeq2dv 14281 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + (((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
43 | 1, 16, 22 | fsumadd 14317 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + (((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) = (Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
44 | 42, 43 | eqtrd 2644 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
45 | 44 | oveq1d 6564 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) − (2 ·
(log‘𝑥)))) |
46 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ 2 ∈ ℂ) |
47 | 8, 14 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℂ) |
48 | 8, 47 | subcld 10271 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) −
(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) |
49 | 1, 46, 48 | fsummulc2 14358 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (2 · Σ𝑛
∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) − (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 ·
(((μ‘𝑛) / 𝑛) − (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) |
50 | 1, 8, 47 | fsumsub 14362 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) − (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
51 | 50 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (2 · Σ𝑛
∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) − (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) |
52 | 49, 51 | eqtr3d 2646 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(2
· (((μ‘𝑛) /
𝑛) −
(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) |
53 | 19, 8 | mulcomd 9940 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · ((μ‘𝑛) / 𝑛)) = (((μ‘𝑛) / 𝑛) · 2)) |
54 | 19, 8, 14 | mul12d 10124 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (((μ‘𝑛) / 𝑛) · (2 · (log‘(𝑥 / 𝑛))))) |
55 | 53, 54 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · ((μ‘𝑛) / 𝑛)) − (2 · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = ((((μ‘𝑛) / 𝑛) · 2) − (((μ‘𝑛) / 𝑛) · (2 · (log‘(𝑥 / 𝑛)))))) |
56 | 19, 8, 47 | subdid 10365 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((μ‘𝑛) / 𝑛) − (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = ((2 · ((μ‘𝑛) / 𝑛)) − (2 · (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) |
57 | 8, 19, 20 | subdid 10365 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · (2 − (2
· (log‘(𝑥 /
𝑛))))) =
((((μ‘𝑛) / 𝑛) · 2) −
(((μ‘𝑛) / 𝑛) · (2 ·
(log‘(𝑥 / 𝑛)))))) |
58 | 55, 56, 57 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (((μ‘𝑛) / 𝑛) − (((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) |
59 | 58 | sumeq2dv 14281 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(2
· (((μ‘𝑛) /
𝑛) −
(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) |
60 | 52, 59 | eqtr3d 2646 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) |
61 | 60 | oveq2d 6565 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) + (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) +
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
62 | 28, 45, 61 | 3eqtr4d 2654 |
. . 3
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) + (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))) |
63 | 62 | mpteq2ia 4668 |
. 2
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) + (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))) |
64 | | ovex 6577 |
. . . . 5
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) ∈
V |
65 | 64 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) ∈
V) |
66 | | ovex 6577 |
. . . . 5
⊢ (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) ∈ V |
67 | 66 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) ∈ V) |
68 | | mulog2sum 25026 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥)))) ∈
𝑂(1) |
69 | 68 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥)))) ∈
𝑂(1)) |
70 | | 2ex 10969 |
. . . . . 6
⊢ 2 ∈
V |
71 | 70 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 2 ∈ V) |
72 | | ovex 6577 |
. . . . . 6
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ V |
73 | 72 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ V) |
74 | | rpssre 11719 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
75 | | o1const 14198 |
. . . . . . 7
⊢
((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 2) ∈ 𝑂(1)) |
76 | 74, 18, 75 | mp2an 704 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ 2) ∈ 𝑂(1) |
77 | 76 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ 2) ∈ 𝑂(1)) |
78 | | reex 9906 |
. . . . . . . . 9
⊢ ℝ
∈ V |
79 | 78, 74 | ssexi 4731 |
. . . . . . . 8
⊢
ℝ+ ∈ V |
80 | 79 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℝ+ ∈ V) |
81 | | sumex 14266 |
. . . . . . . 8
⊢
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ V |
82 | 81 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ V) |
83 | | sumex 14266 |
. . . . . . . 8
⊢
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ V |
84 | 83 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ V) |
85 | | eqidd 2611 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛))) |
86 | | eqidd 2611 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
87 | 80, 82, 84, 85, 86 | offval2 6812 |
. . . . . 6
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∘𝑓 − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) |
88 | | mudivsum 25019 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1) |
89 | | mulogsum 25021 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ 𝑂(1) |
90 | | o1sub 14194 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∘𝑓 − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1)) |
91 | 88, 89, 90 | mp2an 704 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∘𝑓 − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1) |
92 | 87, 91 | syl6eqelr 2697 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1)) |
93 | 71, 73, 77, 92 | o1mul2 14203 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))) ∈ 𝑂(1)) |
94 | 65, 67, 69, 93 | o1add2 14202 |
. . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) + (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))) ∈ 𝑂(1)) |
95 | 94 | trud 1484 |
. 2
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 ·
(log‘𝑥))) + (2
· (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))) ∈ 𝑂(1) |
96 | 63, 95 | eqeltri 2684 |
1
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈
𝑂(1) |