Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . 3
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
2 | | fzfid 12634 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(1...𝐴) ∈
Fin) |
3 | | dvdsssfz1 14878 |
. . . 4
⊢ (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ⊆ (1...𝐴)) |
4 | | ssfi 8065 |
. . . 4
⊢
(((1...𝐴) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝐴} ⊆ (1...𝐴)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ∈ Fin) |
5 | 2, 3, 4 | syl2anc 691 |
. . 3
⊢ (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ∈ Fin) |
6 | | ssrab2 3650 |
. . . 4
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ⊆ ℕ |
7 | 6 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ⊆ ℕ) |
8 | | inss1 3795 |
. . . 4
⊢
((1...𝐴) ∩
ℙ) ⊆ (1...𝐴) |
9 | | ssfi 8065 |
. . . 4
⊢
(((1...𝐴) ∈ Fin
∧ ((1...𝐴) ∩
ℙ) ⊆ (1...𝐴))
→ ((1...𝐴) ∩
ℙ) ∈ Fin) |
10 | 2, 8, 9 | sylancl 693 |
. . 3
⊢ (𝐴 ∈ ℕ →
((1...𝐴) ∩ ℙ)
∈ Fin) |
11 | | pccl 15392 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
12 | 11 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
13 | 12 | nn0zd 11356 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℤ) |
14 | | fznn 12278 |
. . . . . . . 8
⊢ ((𝑝 pCnt 𝐴) ∈ ℤ → (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)))) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)))) |
16 | 15 | anbi2d 736 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))))) |
17 | | an12 834 |
. . . . . . 7
⊢ ((𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)))) |
18 | | prmz 15227 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℤ) |
20 | | iddvdsexp 14843 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℤ ∧ 𝑘 ∈ ℕ) → 𝑝 ∥ (𝑝↑𝑘)) |
21 | 19, 20 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∥ (𝑝↑𝑘)) |
22 | 18 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈
ℤ) |
23 | | prmnn 15226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
24 | 23 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
25 | | nnnn0 11176 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
26 | | nnexpcl 12735 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑘) ∈
ℕ) |
27 | 24, 25, 26 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℕ) |
28 | 27 | nnzd 11357 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℤ) |
29 | | nnz 11276 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
30 | 29 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℤ) |
31 | | dvdstr 14856 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℤ ∧ (𝑝↑𝑘) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝑝 ∥ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ∥ 𝐴) → 𝑝 ∥ 𝐴)) |
32 | 22, 28, 30, 31 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∥ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ∥ 𝐴) → 𝑝 ∥ 𝐴)) |
33 | 21, 32 | mpand 707 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 → 𝑝 ∥ 𝐴)) |
34 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℕ) |
35 | | dvdsle 14870 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℕ) → (𝑝 ∥ 𝐴 → 𝑝 ≤ 𝐴)) |
36 | 22, 34, 35 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝 ∥ 𝐴 → 𝑝 ≤ 𝐴)) |
37 | 33, 36 | syld 46 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 → 𝑝 ≤ 𝐴)) |
38 | 23 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈
ℕ) |
39 | | fznn 12278 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ (1...𝐴) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝐴))) |
40 | 39 | baibd 946 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℕ) → (𝑝 ∈ (1...𝐴) ↔ 𝑝 ≤ 𝐴)) |
41 | 30, 38, 40 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝 ∈ (1...𝐴) ↔ 𝑝 ≤ 𝐴)) |
42 | 37, 41 | sylibrd 248 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 → 𝑝 ∈ (1...𝐴))) |
43 | 42 | pm4.71rd 665 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝↑𝑘) ∥ 𝐴))) |
44 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑝↑𝑘) → (𝑥 ∥ 𝐴 ↔ (𝑝↑𝑘) ∥ 𝐴)) |
45 | 44 | elrab3 3332 |
. . . . . . . . . 10
⊢ ((𝑝↑𝑘) ∈ ℕ → ((𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ↔ (𝑝↑𝑘) ∥ 𝐴)) |
46 | 27, 45 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ↔ (𝑝↑𝑘) ∥ 𝐴)) |
47 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈
ℙ) |
48 | 25 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
ℕ0) |
49 | | pcdvdsb 15411 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝↑𝑘) ∥ 𝐴)) |
50 | 47, 30, 48, 49 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝↑𝑘) ∥ 𝐴)) |
51 | 50 | anbi2d 736 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝↑𝑘) ∥ 𝐴))) |
52 | 43, 46, 51 | 3bitr4rd 300 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)) ↔ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴})) |
53 | 52 | pm5.32da 671 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑘 ∈ ℕ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
54 | 17, 53 | syl5bb 271 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
55 | 16, 54 | bitrd 267 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
56 | 55 | pm5.32da 671 |
. . . 4
⊢ (𝐴 ∈ ℕ → ((𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) ↔ (𝑝 ∈ ℙ ∧ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴})))) |
57 | | elin 3758 |
. . . . . 6
⊢ (𝑝 ∈ ((1...𝐴) ∩ ℙ) ↔ (𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ)) |
58 | 57 | anbi1i 727 |
. . . . 5
⊢ ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ ((𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) |
59 | | anass 679 |
. . . . 5
⊢ (((𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))))) |
60 | | an12 834 |
. . . . 5
⊢ ((𝑝 ∈ (1...𝐴) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) ↔ (𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))))) |
61 | 58, 59, 60 | 3bitri 285 |
. . . 4
⊢ ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))))) |
62 | | anass 679 |
. . . 4
⊢ (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) ↔ (𝑝 ∈ ℙ ∧ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
63 | 56, 61, 62 | 3bitr4g 302 |
. . 3
⊢ (𝐴 ∈ ℕ → ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
64 | 7 | sselda 3568 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) → 𝑛 ∈ ℕ) |
65 | | vmacl 24644 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
66 | 64, 65 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) → (Λ‘𝑛) ∈ ℝ) |
67 | 66 | recnd 9947 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) → (Λ‘𝑛) ∈ ℂ) |
68 | | simprr 792 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ (𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0) |
69 | 1, 5, 7, 10, 63, 67, 68 | fsumvma 24738 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} (Λ‘𝑛) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘))) |
70 | 57 | simprbi 479 |
. . . . . . 7
⊢ (𝑝 ∈ ((1...𝐴) ∩ ℙ) → 𝑝 ∈ ℙ) |
71 | 70 | ad2antlr 759 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → 𝑝 ∈ ℙ) |
72 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) → 𝑘 ∈ ℕ) |
73 | 72 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → 𝑘 ∈ ℕ) |
74 | | vmappw 24642 |
. . . . . 6
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
75 | 71, 73, 74 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
76 | 75 | sumeq2dv 14281 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘)) = Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝)) |
77 | | fzfid 12634 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (1...(𝑝 pCnt 𝐴)) ∈ Fin) |
78 | 70, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝑝 ∈ ((1...𝐴) ∩ ℙ) → 𝑝 ∈ ℕ) |
79 | 78 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
80 | 79 | nnrpd 11746 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
81 | 80 | relogcld 24173 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
82 | 81 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
83 | | fsumconst 14364 |
. . . . 5
⊢
(((1...(𝑝 pCnt 𝐴)) ∈ Fin ∧
(log‘𝑝) ∈
ℂ) → Σ𝑘
∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝) = ((#‘(1...(𝑝 pCnt 𝐴))) · (log‘𝑝))) |
84 | 77, 82, 83 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝) = ((#‘(1...(𝑝 pCnt 𝐴))) · (log‘𝑝))) |
85 | 70, 12 | sylan2 490 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
86 | | hashfz1 12996 |
. . . . . 6
⊢ ((𝑝 pCnt 𝐴) ∈ ℕ0 →
(#‘(1...(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) |
87 | 85, 86 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) →
(#‘(1...(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) |
88 | 87 | oveq1d 6564 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) →
((#‘(1...(𝑝 pCnt
𝐴))) ·
(log‘𝑝)) = ((𝑝 pCnt 𝐴) · (log‘𝑝))) |
89 | 76, 84, 88 | 3eqtrd 2648 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘)) = ((𝑝 pCnt 𝐴) · (log‘𝑝))) |
90 | 89 | sumeq2dv 14281 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘)) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝))) |
91 | | pclogsum 24740 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝)) = (log‘𝐴)) |
92 | 69, 90, 91 | 3eqtrd 2648 |
1
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} (Λ‘𝑛) = (log‘𝐴)) |