Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑑 → (Λ‘𝑛) = (Λ‘𝑑)) |
2 | | oveq2 7221 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑑 → (𝑥 / 𝑛) = (𝑥 / 𝑑)) |
3 | 2 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑑 → (ψ‘(𝑥 / 𝑛)) = (ψ‘(𝑥 / 𝑑))) |
4 | 1, 3 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑑 → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) = ((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑)))) |
5 | 4 | cbvsumv 15260 |
. . . . . . . . . . 11
⊢
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) = Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) |
6 | | fzfid 13546 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑑))) ∈ Fin) |
7 | | elfznn 13141 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
8 | 7 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
9 | | vmacl 26000 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ ℕ →
(Λ‘𝑑) ∈
ℝ) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑑)
∈ ℝ) |
11 | 10 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑑)
∈ ℂ) |
12 | | elfznn 13141 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑))) → 𝑚 ∈
ℕ) |
13 | 12 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) → 𝑚 ∈
ℕ) |
14 | | vmacl 26000 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) →
(Λ‘𝑚) ∈
ℝ) |
16 | 15 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) →
(Λ‘𝑚) ∈
ℂ) |
17 | 6, 11, 16 | fsummulc2 15348 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))(Λ‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((Λ‘𝑑) · (Λ‘𝑚))) |
18 | 7 | nnrpd 12626 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℝ+) |
19 | | rpdivcl 12611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑥 / 𝑑) ∈
ℝ+) |
20 | 18, 19 | sylan2 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ+) |
21 | 20 | rpred 12628 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ) |
22 | | chpval 26004 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 / 𝑑) ∈ ℝ → (ψ‘(𝑥 / 𝑑)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))(Λ‘𝑚)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑑)) = Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))(Λ‘𝑚)) |
24 | 23 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (ψ‘(𝑥 /
𝑑))) =
((Λ‘𝑑)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))(Λ‘𝑚))) |
25 | 13 | nncnd 11846 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) → 𝑚 ∈
ℂ) |
26 | 7 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) → 𝑑 ∈
ℕ) |
27 | 26 | nncnd 11846 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) → 𝑑 ∈
ℂ) |
28 | 26 | nnne0d 11880 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) → 𝑑 ≠ 0) |
29 | 25, 27, 28 | divcan3d 11613 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) → ((𝑑 · 𝑚) / 𝑑) = 𝑚) |
30 | 29 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) →
(Λ‘((𝑑
· 𝑚) / 𝑑)) = (Λ‘𝑚)) |
31 | 30 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) →
((Λ‘𝑑)
· (Λ‘((𝑑 · 𝑚) / 𝑑))) = ((Λ‘𝑑) · (Λ‘𝑚))) |
32 | 31 | sumeq2dv 15267 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))((Λ‘𝑑) ·
(Λ‘((𝑑
· 𝑚) / 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((Λ‘𝑑) · (Λ‘𝑚))) |
33 | 17, 24, 32 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑑)
· (ψ‘(𝑥 /
𝑑))) = Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))((Λ‘𝑑) ·
(Λ‘((𝑑
· 𝑚) / 𝑑)))) |
34 | 33 | sumeq2dv 15267 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))((Λ‘𝑑) · (ψ‘(𝑥 / 𝑑))) = Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((Λ‘𝑑) · (Λ‘((𝑑 · 𝑚) / 𝑑)))) |
35 | 5, 34 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) = Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((Λ‘𝑑) · (Λ‘((𝑑 · 𝑚) / 𝑑)))) |
36 | | fvoveq1 7236 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑑 · 𝑚) → (Λ‘(𝑛 / 𝑑)) = (Λ‘((𝑑 · 𝑚) / 𝑑))) |
37 | 36 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑑 · 𝑚) → ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) = ((Λ‘𝑑) · (Λ‘((𝑑 · 𝑚) / 𝑑)))) |
38 | | rpre 12594 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
39 | | ssrab2 3993 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ ℕ |
40 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
41 | 39, 40 | sseldi 3899 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → 𝑑 ∈ ℕ) |
42 | 41 | anassrs 471 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑑 ∈ ℕ) |
43 | 42, 9 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘𝑑) ∈ ℝ) |
44 | | elfznn 13141 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
45 | 44 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
46 | | dvdsdivcl 15877 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑑) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
47 | 45, 46 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑑) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
48 | 39, 47 | sseldi 3899 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑑) ∈ ℕ) |
49 | | vmacl 26000 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 / 𝑑) ∈ ℕ →
(Λ‘(𝑛 / 𝑑)) ∈
ℝ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘(𝑛 / 𝑑)) ∈ ℝ) |
51 | 43, 50 | remulcld 10863 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) ∈ ℝ) |
52 | 51 | recnd 10861 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) ∈ ℂ) |
53 | 52 | anasss 470 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → ((Λ‘𝑑) ·
(Λ‘(𝑛 / 𝑑))) ∈
ℂ) |
54 | 37, 38, 53 | dvdsflsumcom 26070 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) = Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((Λ‘𝑑) · (Λ‘((𝑑 · 𝑚) / 𝑑)))) |
55 | 35, 54 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑)))) |
56 | 55 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)))) |
57 | | fzfid 13546 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
58 | | vmacl 26000 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
59 | 45, 58 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
60 | 59 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
61 | 44 | nnrpd 12626 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
62 | | rpdivcl 12611 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
63 | 61, 62 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
64 | 63 | rpred 12628 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
65 | | chpcl 26006 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ → (ψ‘(𝑥 / 𝑛)) ∈ ℝ) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑛)) ∈
ℝ) |
67 | 66 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑛)) ∈
ℂ) |
68 | 60, 67 | mulcld 10853 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ∈
ℂ) |
69 | 45 | nnrpd 12626 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
70 | | relogcl 25464 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℝ) |
72 | 71 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℂ) |
73 | 60, 72 | mulcld 10853 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (log‘𝑛))
∈ ℂ) |
74 | 57, 68, 73 | fsumadd 15304 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) + ((Λ‘𝑛) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)))) |
75 | | fzfid 13546 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...𝑛) ∈
Fin) |
76 | | dvdsssfz1 15879 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
77 | 45, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
78 | 75, 77 | ssfid 8898 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ∈ Fin) |
79 | 78, 51 | fsumrecl 15298 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑑 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑑) ·
(Λ‘(𝑛 / 𝑑))) ∈
ℝ) |
80 | 79 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑑 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑑) ·
(Λ‘(𝑛 / 𝑑))) ∈
ℂ) |
81 | 57, 80, 73 | fsumadd 15304 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) + ((Λ‘𝑛) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)))) |
82 | 56, 74, 81 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) + ((Λ‘𝑛) · (log‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) + ((Λ‘𝑛) · (log‘𝑛)))) |
83 | 72, 67 | addcomd 11034 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛))) = ((ψ‘(𝑥 / 𝑛)) + (log‘𝑛))) |
84 | 83 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛)))) = ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) + (log‘𝑛)))) |
85 | 60, 67, 72 | adddid 10857 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((ψ‘(𝑥 /
𝑛)) + (log‘𝑛))) = (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) + ((Λ‘𝑛) · (log‘𝑛)))) |
86 | 84, 85 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝑥 / 𝑛)))) = (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) + ((Λ‘𝑛) · (log‘𝑛)))) |
87 | 86 | sumeq2dv 15267 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) + ((Λ‘𝑛) · (log‘𝑛)))) |
88 | | logsqvma2 26424 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) + ((Λ‘𝑛) · (log‘𝑛)))) |
89 | 45, 88 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑑 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) + ((Λ‘𝑛) · (log‘𝑛)))) |
90 | 89 | sumeq2dv 15267 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑑) · (Λ‘(𝑛 / 𝑑))) + ((Λ‘𝑛) · (log‘𝑛)))) |
91 | 82, 87, 90 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2))) |
92 | | fvoveq1 7236 |
. . . . . . . . 9
⊢ (𝑛 = (𝑑 · 𝑚) → (log‘(𝑛 / 𝑑)) = (log‘((𝑑 · 𝑚) / 𝑑))) |
93 | 92 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑛 = (𝑑 · 𝑚) → ((log‘(𝑛 / 𝑑))↑2) = ((log‘((𝑑 · 𝑚) / 𝑑))↑2)) |
94 | 93 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑛 = (𝑑 · 𝑚) → ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) = ((μ‘𝑑) · ((log‘((𝑑 · 𝑚) / 𝑑))↑2))) |
95 | | mucl 26023 |
. . . . . . . . . 10
⊢ (𝑑 ∈ ℕ →
(μ‘𝑑) ∈
ℤ) |
96 | 41, 95 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → (μ‘𝑑) ∈ ℤ) |
97 | 96 | zcnd 12283 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → (μ‘𝑑) ∈ ℂ) |
98 | 61 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → 𝑛 ∈ ℝ+) |
99 | 41 | nnrpd 12626 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → 𝑑 ∈ ℝ+) |
100 | 98, 99 | rpdivcld 12645 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → (𝑛 / 𝑑) ∈
ℝ+) |
101 | | relogcl 25464 |
. . . . . . . . . . 11
⊢ ((𝑛 / 𝑑) ∈ ℝ+ →
(log‘(𝑛 / 𝑑)) ∈
ℝ) |
102 | 101 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝑛 / 𝑑) ∈ ℝ+ →
(log‘(𝑛 / 𝑑)) ∈
ℂ) |
103 | 100, 102 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → (log‘(𝑛 / 𝑑)) ∈ ℂ) |
104 | 103 | sqcld 13714 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → ((log‘(𝑛 / 𝑑))↑2) ∈ ℂ) |
105 | 97, 104 | mulcld 10853 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) ∈ ℂ) |
106 | 94, 38, 105 | dvdsflsumcom 26070 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) = Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘((𝑑 · 𝑚) / 𝑑))↑2))) |
107 | 29 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) →
(log‘((𝑑 ·
𝑚) / 𝑑)) = (log‘𝑚)) |
108 | 107 | oveq1d 7228 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) →
((log‘((𝑑 ·
𝑚) / 𝑑))↑2) = ((log‘𝑚)↑2)) |
109 | 108 | oveq2d 7229 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))) →
((μ‘𝑑) ·
((log‘((𝑑 ·
𝑚) / 𝑑))↑2)) = ((μ‘𝑑) · ((log‘𝑚)↑2))) |
110 | 109 | sumeq2dv 15267 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑑)))((μ‘𝑑) · ((log‘((𝑑 · 𝑚) / 𝑑))↑2)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘𝑚)↑2))) |
111 | 110 | sumeq2dv 15267 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘((𝑑 · 𝑚) / 𝑑))↑2)) = Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘𝑚)↑2))) |
112 | 91, 106, 111 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) = Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘𝑚)↑2))) |
113 | 112 | oveq1d 7228 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) = (Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘𝑚)↑2)) / 𝑥)) |
114 | 113 | oveq1d 7228 |
. . 3
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) = ((Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) |
115 | 114 | mpteq2ia 5146 |
. 2
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) |
116 | | eqid 2737 |
. . 3
⊢
((((log‘(𝑥 /
𝑑))↑2) + (2 − (2
· (log‘(𝑥 /
𝑑))))) / 𝑑) = ((((log‘(𝑥 / 𝑑))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑑))))) / 𝑑) |
117 | 116 | selberglem2 26427 |
. 2
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑑)))((μ‘𝑑) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
118 | 115, 117 | eqeltri 2834 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |