Step | Hyp | Ref
| Expression |
1 | | pntsval.1 |
. . 3
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
2 | 1 | pntsval 25061 |
. 2
⊢ (𝐴 ∈ ℝ → (𝑆‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝐴 / 𝑛))))) |
3 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
5 | | vmacl 24644 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℝ) |
7 | 6 | recnd 9947 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℂ) |
8 | 4 | nnrpd 11746 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℝ+) |
9 | 8 | relogcld 24173 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℝ) |
10 | 9 | recnd 9947 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℂ) |
11 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
12 | 11, 4 | nndivred 10946 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (𝐴 / 𝑛) ∈
ℝ) |
13 | | chpcl 24650 |
. . . . . 6
⊢ ((𝐴 / 𝑛) ∈ ℝ → (ψ‘(𝐴 / 𝑛)) ∈ ℝ) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (ψ‘(𝐴 /
𝑛)) ∈
ℝ) |
15 | 14 | recnd 9947 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (ψ‘(𝐴 /
𝑛)) ∈
ℂ) |
16 | 7, 10, 15 | adddid 9943 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑛)
· ((log‘𝑛) +
(ψ‘(𝐴 / 𝑛)))) = (((Λ‘𝑛) · (log‘𝑛)) + ((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛))))) |
17 | 16 | sumeq2dv 14281 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝐴 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) · (log‘𝑛)) + ((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛))))) |
18 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (Λ‘𝑛) = (Λ‘𝑚)) |
19 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝐴 / 𝑛) = (𝐴 / 𝑚)) |
20 | 19 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (ψ‘(𝐴 / 𝑛)) = (ψ‘(𝐴 / 𝑚))) |
21 | 18, 20 | oveq12d 6567 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛))) = ((Λ‘𝑚) · (ψ‘(𝐴 / 𝑚)))) |
22 | 21 | cbvsumv 14274 |
. . . . 5
⊢
Σ𝑛 ∈
(1...(⌊‘𝐴))((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛))) = Σ𝑚 ∈ (1...(⌊‘𝐴))((Λ‘𝑚) · (ψ‘(𝐴 / 𝑚))) |
23 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (1...(⌊‘(𝐴 / 𝑚))) ∈ Fin) |
24 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℕ) |
25 | 24 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ 𝑚 ∈
ℕ) |
26 | | vmacl 24644 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑚)
∈ ℝ) |
28 | 27 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑚)
∈ ℂ) |
29 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚))) → 𝑘 ∈
ℕ) |
30 | 29 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) → 𝑘 ∈
ℕ) |
31 | | vmacl 24644 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) →
(Λ‘𝑘) ∈
ℝ) |
33 | 32 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) →
(Λ‘𝑘) ∈
ℂ) |
34 | 23, 28, 33 | fsummulc2 14358 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑚)
· Σ𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))(Λ‘𝑘)) = Σ𝑘 ∈ (1...(⌊‘(𝐴 / 𝑚)))((Λ‘𝑚) · (Λ‘𝑘))) |
35 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
36 | 35, 25 | nndivred 10946 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (𝐴 / 𝑚) ∈
ℝ) |
37 | | chpval 24648 |
. . . . . . . . . 10
⊢ ((𝐴 / 𝑚) ∈ ℝ → (ψ‘(𝐴 / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘(𝐴 / 𝑚)))(Λ‘𝑘)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (ψ‘(𝐴 /
𝑚)) = Σ𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))(Λ‘𝑘)) |
39 | 38 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑚)
· (ψ‘(𝐴 /
𝑚))) =
((Λ‘𝑚)
· Σ𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))(Λ‘𝑘))) |
40 | 30 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) → 𝑘 ∈
ℂ) |
41 | 24 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) → 𝑚 ∈
ℕ) |
42 | 41 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) → 𝑚 ∈
ℂ) |
43 | 41 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) → 𝑚 ≠ 0) |
44 | 40, 42, 43 | divcan3d 10685 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) → ((𝑚 · 𝑘) / 𝑚) = 𝑘) |
45 | 44 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) →
(Λ‘((𝑚
· 𝑘) / 𝑚)) = (Λ‘𝑘)) |
46 | 45 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
∧ 𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))) →
((Λ‘𝑚)
· (Λ‘((𝑚 · 𝑘) / 𝑚))) = ((Λ‘𝑚) · (Λ‘𝑘))) |
47 | 46 | sumeq2dv 14281 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ Σ𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))((Λ‘𝑚) ·
(Λ‘((𝑚
· 𝑘) / 𝑚))) = Σ𝑘 ∈ (1...(⌊‘(𝐴 / 𝑚)))((Λ‘𝑚) · (Λ‘𝑘))) |
48 | 34, 39, 47 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑚)
· (ψ‘(𝐴 /
𝑚))) = Σ𝑘 ∈
(1...(⌊‘(𝐴 /
𝑚)))((Λ‘𝑚) ·
(Λ‘((𝑚
· 𝑘) / 𝑚)))) |
49 | 48 | sumeq2dv 14281 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
Σ𝑚 ∈
(1...(⌊‘𝐴))((Λ‘𝑚) · (ψ‘(𝐴 / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘𝐴))Σ𝑘 ∈ (1...(⌊‘(𝐴 / 𝑚)))((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) |
50 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑛 = (𝑚 · 𝑘) → (𝑛 / 𝑚) = ((𝑚 · 𝑘) / 𝑚)) |
51 | 50 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 · 𝑘) → (Λ‘(𝑛 / 𝑚)) = (Λ‘((𝑚 · 𝑘) / 𝑚))) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑛 = (𝑚 · 𝑘) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) = ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) |
53 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
54 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ ℕ |
55 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
56 | 54, 55 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ ℕ) |
57 | 56, 26 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘𝑚) ∈ ℝ) |
58 | | dvdsdivcl 14876 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
59 | 4, 58 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
60 | 54, 59 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ ℕ) |
61 | | vmacl 24644 |
. . . . . . . . . . 11
⊢ ((𝑛 / 𝑚) ∈ ℕ →
(Λ‘(𝑛 / 𝑚)) ∈
ℝ) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ) |
63 | 57, 62 | remulcld 9949 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ) |
64 | 63 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ) |
65 | 64 | anasss 677 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) ∈
ℂ) |
66 | 52, 53, 65 | dvdsflsumcom 24714 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘𝐴))Σ𝑘 ∈ (1...(⌊‘(𝐴 / 𝑚)))((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) |
67 | 49, 66 | eqtr4d 2647 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
Σ𝑚 ∈
(1...(⌊‘𝐴))((Λ‘𝑚) · (ψ‘(𝐴 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
68 | 22, 67 | syl5eq 2656 |
. . . 4
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
69 | 68 | oveq2d 6565 |
. . 3
⊢ (𝐴 ∈ ℝ →
(Σ𝑛 ∈
(1...(⌊‘𝐴))((Λ‘𝑛) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
70 | | fzfid 12634 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(1...(⌊‘𝐴))
∈ Fin) |
71 | 7, 10 | mulcld 9939 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑛)
· (log‘𝑛))
∈ ℂ) |
72 | 7, 15 | mulcld 9939 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑛)
· (ψ‘(𝐴 /
𝑛))) ∈
ℂ) |
73 | 70, 71, 72 | fsumadd 14317 |
. . 3
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(((Λ‘𝑛) · (log‘𝑛)) + ((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛))))) |
74 | | fzfid 12634 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (1...𝑛) ∈
Fin) |
75 | | dvdsssfz1 14878 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
76 | 4, 75 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
77 | | ssfi 8065 |
. . . . . . 7
⊢
(((1...𝑛) ∈ Fin
∧ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ∈ Fin) |
78 | 74, 76, 77 | syl2anc 691 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ∈ Fin) |
79 | 78, 63 | fsumrecl 14312 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) ∈
ℝ) |
80 | 79 | recnd 9947 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) ∈
ℂ) |
81 | 70, 71, 80 | fsumadd 14317 |
. . 3
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
82 | 69, 73, 81 | 3eqtr4d 2654 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(((Λ‘𝑛) · (log‘𝑛)) + ((Λ‘𝑛) · (ψ‘(𝐴 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
83 | 2, 17, 82 | 3eqtrd 2648 |
1
⊢ (𝐴 ∈ ℝ → (𝑆‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |