Proof of Theorem selbergr
Step | Hyp | Ref
| Expression |
1 | | reex 10825 |
. . . . . . 7
⊢ ℝ
∈ V |
2 | | rpssre 12598 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
3 | 1, 2 | ssexi 5220 |
. . . . . 6
⊢
ℝ+ ∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ+ ∈ V) |
5 | | ovexd 7253 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) ∈ V) |
6 | | ovexd 7253 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)) ∈ V) |
7 | | eqidd 2738 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))))) |
8 | | eqidd 2738 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) |
9 | 4, 5, 6, 7, 8 | offval2 7493 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘f −
(𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))))) |
10 | 9 | mptru 1550 |
. . 3
⊢ ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘f −
(𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) |
11 | | pntrval.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
12 | 11 | pntrf 26449 |
. . . . . . . . . . 11
⊢ 𝑅:ℝ+⟶ℝ |
13 | 12 | ffvelrni 6908 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
14 | 13 | recnd 10866 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℂ) |
15 | | relogcl 25469 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
16 | 15 | recnd 10866 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
17 | 14, 16 | mulcld 10858 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((𝑅‘𝑥) · (log‘𝑥)) ∈
ℂ) |
18 | | fzfid 13551 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
19 | | elfznn 13146 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
20 | 19 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
21 | | vmacl 26005 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ℕ →
(Λ‘𝑑) ∈
ℝ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑑)
∈ ℝ) |
23 | 22 | recnd 10866 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑑)
∈ ℂ) |
24 | | rpre 12599 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
25 | | nndivre 11876 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑥 / 𝑑) ∈ ℝ) |
26 | 24, 19, 25 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ) |
27 | | chpcl 26011 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑑) ∈ ℝ → (ψ‘(𝑥 / 𝑑)) ∈ ℝ) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑑)) ∈
ℝ) |
29 | 28 | recnd 10866 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑑)) ∈
ℂ) |
30 | 23, 29 | mulcld 10858 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (ψ‘(𝑥 /
𝑑))) ∈
ℂ) |
31 | 18, 30 | fsumcl 15302 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) ∈ ℂ) |
32 | 17, 31 | addcld 10857 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ) |
33 | | rpcn 12601 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
34 | | rpne0 12607 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
35 | 32, 33, 34 | divcld 11613 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) ∈ ℂ) |
36 | 22, 20 | nndivred 11889 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
/ 𝑑) ∈
ℝ) |
37 | 36 | recnd 10866 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
/ 𝑑) ∈
ℂ) |
38 | 18, 37 | fsumcl 15302 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) ∈ ℂ) |
39 | 35, 38, 16 | nnncan2d 11229 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) |
40 | | chpcl 26011 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
41 | 24, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
42 | 41 | recnd 10866 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℂ) |
43 | 42, 16 | mulcld 10858 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘𝑥))
∈ ℂ) |
44 | 43, 31 | addcld 10857 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ) |
45 | 44, 33, 34 | divcld 11613 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) ∈ ℂ) |
46 | 45, 16, 16 | subsub4d 11225 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (log‘𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((log‘𝑥) + (log‘𝑥)))) |
47 | 11 | pntrval 26448 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
48 | 47 | oveq1d 7233 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((𝑅‘𝑥) · (log‘𝑥)) = (((ψ‘𝑥) − 𝑥) · (log‘𝑥))) |
49 | 42, 33, 16 | subdird 11294 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
− 𝑥) ·
(log‘𝑥)) =
(((ψ‘𝑥) ·
(log‘𝑥)) −
(𝑥 ·
(log‘𝑥)))) |
50 | 48, 49 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((𝑅‘𝑥) · (log‘𝑥)) = (((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥)))) |
51 | 50 | oveq1d 7233 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) = ((((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))))) |
52 | 33, 16 | mulcld 10858 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ·
(log‘𝑥)) ∈
ℂ) |
53 | 43, 31, 52 | addsubd 11215 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) = ((((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))))) |
54 | 51, 53 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) = ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥)))) |
55 | 54 | oveq1d 7233 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) / 𝑥)) |
56 | | rpcnne0 12609 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
57 | | divsubdir 11531 |
. . . . . . . . . 10
⊢
(((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ ∧ (𝑥 · (log‘𝑥)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · (log‘𝑥)) / 𝑥))) |
58 | 44, 52, 56, 57 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · (log‘𝑥)) / 𝑥))) |
59 | 16, 33, 34 | divcan3d 11618 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((𝑥 ·
(log‘𝑥)) / 𝑥) = (log‘𝑥)) |
60 | 59 | oveq2d 7234 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · (log‘𝑥)) / 𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥))) |
61 | 55, 58, 60 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥))) |
62 | 61 | oveq1d 7233 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) = ((((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (log‘𝑥))) |
63 | 16 | 2timesd 12078 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (2 · (log‘𝑥)) = ((log‘𝑥) + (log‘𝑥))) |
64 | 63 | oveq2d 7234 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((log‘𝑥) + (log‘𝑥)))) |
65 | 46, 62, 64 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) |
66 | 65 | oveq1d 7233 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = ((((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) |
67 | 33, 38 | mulcld 10858 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) ∈ ℂ) |
68 | | divsubdir 11531 |
. . . . . . 7
⊢
(((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ ∧ (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) / 𝑥) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥))) |
69 | 32, 67, 56, 68 | syl3anc 1373 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) / 𝑥) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥))) |
70 | 17, 31, 67 | addsubassd 11214 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = (((𝑅‘𝑥) · (log‘𝑥)) + (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))))) |
71 | 33 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
72 | 71, 37 | mulcld 10858 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ·
((Λ‘𝑑) / 𝑑)) ∈
ℂ) |
73 | 18, 30, 72 | fsumsub 15357 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))(((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − Σ𝑑 ∈ (1...(⌊‘𝑥))(𝑥 · ((Λ‘𝑑) / 𝑑)))) |
74 | 26 | recnd 10866 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℂ) |
75 | 23, 29, 74 | subdid 11293 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· ((ψ‘(𝑥 /
𝑑)) − (𝑥 / 𝑑))) = (((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − ((Λ‘𝑑) · (𝑥 / 𝑑)))) |
76 | 19 | nnrpd 12631 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℝ+) |
77 | | rpdivcl 12616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑥 / 𝑑) ∈
ℝ+) |
78 | 76, 77 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ+) |
79 | 11 | pntrval 26448 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 / 𝑑) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑑)) = ((ψ‘(𝑥 / 𝑑)) − (𝑥 / 𝑑))) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / 𝑑)) = ((ψ‘(𝑥 / 𝑑)) − (𝑥 / 𝑑))) |
81 | 80 | oveq2d 7234 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (𝑅‘(𝑥 / 𝑑))) = ((Λ‘𝑑) · ((ψ‘(𝑥 / 𝑑)) − (𝑥 / 𝑑)))) |
82 | 20 | nnrpd 12631 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
83 | | rpcnne0 12609 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ ℝ+
→ (𝑑 ∈ ℂ
∧ 𝑑 ≠
0)) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑑 ∈ ℂ
∧ 𝑑 ≠
0)) |
85 | | div12 11517 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(Λ‘𝑑) ∈
ℂ ∧ (𝑑 ∈
ℂ ∧ 𝑑 ≠ 0))
→ (𝑥 ·
((Λ‘𝑑) / 𝑑)) = ((Λ‘𝑑) · (𝑥 / 𝑑))) |
86 | 71, 23, 84, 85 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ·
((Λ‘𝑑) / 𝑑)) = ((Λ‘𝑑) · (𝑥 / 𝑑))) |
87 | 86 | oveq2d 7234 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑑)
· (ψ‘(𝑥 /
𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑))) = (((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − ((Λ‘𝑑) · (𝑥 / 𝑑)))) |
88 | 75, 81, 87 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (𝑅‘(𝑥 / 𝑑))) = (((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑)))) |
89 | 88 | sumeq2dv 15272 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑))) = Σ𝑑 ∈ (1...(⌊‘𝑥))(((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑)))) |
90 | 18, 33, 37 | fsummulc2 15353 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝑥 · ((Λ‘𝑑) / 𝑑))) |
91 | 90 | oveq2d 7234 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − Σ𝑑 ∈ (1...(⌊‘𝑥))(𝑥 · ((Λ‘𝑑) / 𝑑)))) |
92 | 73, 89, 91 | 3eqtr4rd 2788 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) |
93 | 92 | oveq2d 7234 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)))) = (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑))))) |
94 | 70, 93 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑))))) |
95 | 94 | oveq1d 7233 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) / 𝑥) = ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
96 | 38, 33, 34 | divcan3d 11618 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((𝑥 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥) = Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) |
97 | 96 | oveq2d 7234 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥)) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) |
98 | 69, 95, 97 | 3eqtr3rd 2786 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) = ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
99 | 39, 66, 98 | 3eqtr3d 2785 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
100 | 99 | mpteq2ia 5151 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ ((((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
101 | 10, 100 | eqtri 2765 |
. 2
⊢ ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘f −
(𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
102 | | selberg2 26437 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
103 | | vmadivsum 26368 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) ∈ 𝑂(1) |
104 | | o1sub 15182 |
. . 3
⊢ (((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) ∧
(𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘f −
(𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) ∈ 𝑂(1)) |
105 | 102, 103,
104 | mp2an 692 |
. 2
⊢ ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘f −
(𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) ∈ 𝑂(1) |
106 | 101, 105 | eqeltrri 2835 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) ∈ 𝑂(1) |