Proof of Theorem selbergr
Step | Hyp | Ref
| Expression |
1 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
2 | | rpssre 11719 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
3 | 1, 2 | ssexi 4731 |
. . . . . 6
⊢
ℝ+ ∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ+ ∈ V) |
5 | | ovex 6577 |
. . . . . 6
⊢
(((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) ∈ V |
6 | 5 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) ∈ V) |
7 | | ovex 6577 |
. . . . . 6
⊢
(Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)) ∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)) ∈ V) |
9 | | eqidd 2611 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))))) |
10 | | eqidd 2611 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) |
11 | 4, 6, 8, 9, 10 | offval2 6812 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘𝑓
− (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))))) |
12 | 11 | trud 1484 |
. . 3
⊢ ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘𝑓
− (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) |
13 | | pntrval.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
14 | 13 | pntrf 25052 |
. . . . . . . . . . 11
⊢ 𝑅:ℝ+⟶ℝ |
15 | 14 | ffvelrni 6266 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
16 | 15 | recnd 9947 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℂ) |
17 | | relogcl 24126 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
18 | 17 | recnd 9947 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
19 | 16, 18 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((𝑅‘𝑥) · (log‘𝑥)) ∈
ℂ) |
20 | | fzfid 12634 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
21 | | elfznn 12241 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
22 | 21 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
23 | | vmacl 24644 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ℕ →
(Λ‘𝑑) ∈
ℝ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑑)
∈ ℝ) |
25 | 24 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑑)
∈ ℂ) |
26 | | rpre 11715 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
27 | | nndivre 10933 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑥 / 𝑑) ∈ ℝ) |
28 | 26, 21, 27 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ) |
29 | | chpcl 24650 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑑) ∈ ℝ → (ψ‘(𝑥 / 𝑑)) ∈ ℝ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑑)) ∈
ℝ) |
31 | 30 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑑)) ∈
ℂ) |
32 | 25, 31 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (ψ‘(𝑥 /
𝑑))) ∈
ℂ) |
33 | 20, 32 | fsumcl 14311 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) ∈ ℂ) |
34 | 19, 33 | addcld 9938 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ) |
35 | | rpcn 11717 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
36 | | rpne0 11724 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
37 | 34, 35, 36 | divcld 10680 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) ∈ ℂ) |
38 | 24, 22 | nndivred 10946 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
/ 𝑑) ∈
ℝ) |
39 | 38 | recnd 9947 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
/ 𝑑) ∈
ℂ) |
40 | 20, 39 | fsumcl 14311 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) ∈ ℂ) |
41 | 37, 40, 18 | nnncan2d 10306 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) |
42 | | chpcl 24650 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
43 | 26, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
44 | 43 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℂ) |
45 | 44, 18 | mulcld 9939 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘𝑥))
∈ ℂ) |
46 | 45, 33 | addcld 9938 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ) |
47 | 46, 35, 36 | divcld 10680 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) ∈ ℂ) |
48 | 47, 18, 18 | subsub4d 10302 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (log‘𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((log‘𝑥) + (log‘𝑥)))) |
49 | 13 | pntrval 25051 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
50 | 49 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((𝑅‘𝑥) · (log‘𝑥)) = (((ψ‘𝑥) − 𝑥) · (log‘𝑥))) |
51 | 44, 35, 18 | subdird 10366 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
− 𝑥) ·
(log‘𝑥)) =
(((ψ‘𝑥) ·
(log‘𝑥)) −
(𝑥 ·
(log‘𝑥)))) |
52 | 50, 51 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((𝑅‘𝑥) · (log‘𝑥)) = (((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥)))) |
53 | 52 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) = ((((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))))) |
54 | 35, 18 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ·
(log‘𝑥)) ∈
ℂ) |
55 | 45, 33, 54 | addsubd 10292 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) = ((((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))))) |
56 | 53, 55 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) = ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥)))) |
57 | 56 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) / 𝑥)) |
58 | | rpcnne0 11726 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
59 | | divsubdir 10600 |
. . . . . . . . . 10
⊢
(((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ ∧ (𝑥 · (log‘𝑥)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · (log‘𝑥)) / 𝑥))) |
60 | 46, 54, 58, 59 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · (log‘𝑥))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · (log‘𝑥)) / 𝑥))) |
61 | 18, 35, 36 | divcan3d 10685 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((𝑥 ·
(log‘𝑥)) / 𝑥) = (log‘𝑥)) |
62 | 61 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · (log‘𝑥)) / 𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥))) |
63 | 57, 60, 62 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥))) |
64 | 63 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) = ((((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (log‘𝑥))) |
65 | 18 | 2timesd 11152 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (2 · (log‘𝑥)) = ((log‘𝑥) + (log‘𝑥))) |
66 | 65 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((log‘𝑥) + (log‘𝑥)))) |
67 | 48, 64, 66 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) |
68 | 67 | oveq1d 6564 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (log‘𝑥)) − (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = ((((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) |
69 | 35, 40 | mulcld 9939 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) ∈ ℂ) |
70 | | divsubdir 10600 |
. . . . . . 7
⊢
(((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) ∈ ℂ ∧ (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) / 𝑥) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥))) |
71 | 34, 69, 58, 70 | syl3anc 1318 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) / 𝑥) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥))) |
72 | 19, 33, 69 | addsubassd 10291 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = (((𝑅‘𝑥) · (log‘𝑥)) + (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))))) |
73 | 35 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
74 | 73, 39 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ·
((Λ‘𝑑) / 𝑑)) ∈
ℂ) |
75 | 20, 32, 74 | fsumsub 14362 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))(((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − Σ𝑑 ∈ (1...(⌊‘𝑥))(𝑥 · ((Λ‘𝑑) / 𝑑)))) |
76 | 28 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℂ) |
77 | 25, 31, 76 | subdid 10365 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· ((ψ‘(𝑥 /
𝑑)) − (𝑥 / 𝑑))) = (((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − ((Λ‘𝑑) · (𝑥 / 𝑑)))) |
78 | 21 | nnrpd 11746 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℝ+) |
79 | | rpdivcl 11732 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑥 / 𝑑) ∈
ℝ+) |
80 | 78, 79 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ+) |
81 | 13 | pntrval 25051 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 / 𝑑) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑑)) = ((ψ‘(𝑥 / 𝑑)) − (𝑥 / 𝑑))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / 𝑑)) = ((ψ‘(𝑥 / 𝑑)) − (𝑥 / 𝑑))) |
83 | 82 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (𝑅‘(𝑥 / 𝑑))) = ((Λ‘𝑑) · ((ψ‘(𝑥 / 𝑑)) − (𝑥 / 𝑑)))) |
84 | 22 | nnrpd 11746 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
85 | | rpcnne0 11726 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ ℝ+
→ (𝑑 ∈ ℂ
∧ 𝑑 ≠
0)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑑 ∈ ℂ
∧ 𝑑 ≠
0)) |
87 | | div12 10586 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(Λ‘𝑑) ∈
ℂ ∧ (𝑑 ∈
ℂ ∧ 𝑑 ≠ 0))
→ (𝑥 ·
((Λ‘𝑑) / 𝑑)) = ((Λ‘𝑑) · (𝑥 / 𝑑))) |
88 | 73, 25, 86, 87 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ·
((Λ‘𝑑) / 𝑑)) = ((Λ‘𝑑) · (𝑥 / 𝑑))) |
89 | 88 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑑)
· (ψ‘(𝑥 /
𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑))) = (((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − ((Λ‘𝑑) · (𝑥 / 𝑑)))) |
90 | 77, 83, 89 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (𝑅‘(𝑥 / 𝑑))) = (((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑)))) |
91 | 90 | sumeq2dv 14281 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑))) = Σ𝑑 ∈ (1...(⌊‘𝑥))(((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · ((Λ‘𝑑) / 𝑑)))) |
92 | 20, 35, 39 | fsummulc2 14358 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝑥 · ((Λ‘𝑑) / 𝑑))) |
93 | 92 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − Σ𝑑 ∈ (1...(⌊‘𝑥))(𝑥 · ((Λ‘𝑑) / 𝑑)))) |
94 | 75, 91, 93 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) |
95 | 94 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (((𝑅‘𝑥) · (log‘𝑥)) + (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)))) = (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑))))) |
96 | 72, 95 | eqtrd 2644 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) = (((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑))))) |
97 | 96 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) − (𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) / 𝑥) = ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
98 | 40, 35, 36 | divcan3d 10685 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((𝑥 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥) = Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) |
99 | 98 | oveq2d 6565 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − ((𝑥 · Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) / 𝑥)) = (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑))) |
100 | 71, 97, 99 | 3eqtr3rd 2653 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑)) = ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
101 | 41, 68, 100 | 3eqtr3d 2652 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) = ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
102 | 101 | mpteq2ia 4668 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ ((((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥))) − (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
103 | 12, 102 | eqtri 2632 |
. 2
⊢ ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘𝑓
− (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) |
104 | | selberg2 25040 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
105 | | vmadivsum 24971 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) ∈ 𝑂(1) |
106 | | o1sub 14194 |
. . 3
⊢ (((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) ∧
(𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘𝑓
− (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) ∈ 𝑂(1)) |
107 | 104, 105,
106 | mp2an 704 |
. 2
⊢ ((𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) / 𝑥) − (2 · (log‘𝑥)))) ∘𝑓
− (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) / 𝑑) − (log‘𝑥)))) ∈ 𝑂(1) |
108 | 103, 107 | eqeltrri 2685 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) ∈ 𝑂(1) |