| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . 3
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
| 2 | | dvdsfi 16826 |
. . 3
⊢ (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ∈ Fin) |
| 3 | | ssrab2 4080 |
. . . 4
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ⊆ ℕ |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ⊆ ℕ) |
| 5 | | fzfid 14014 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(1...𝐴) ∈
Fin) |
| 6 | | inss1 4237 |
. . . 4
⊢
((1...𝐴) ∩
ℙ) ⊆ (1...𝐴) |
| 7 | | ssfi 9213 |
. . . 4
⊢
(((1...𝐴) ∈ Fin
∧ ((1...𝐴) ∩
ℙ) ⊆ (1...𝐴))
→ ((1...𝐴) ∩
ℙ) ∈ Fin) |
| 8 | 5, 6, 7 | sylancl 586 |
. . 3
⊢ (𝐴 ∈ ℕ →
((1...𝐴) ∩ ℙ)
∈ Fin) |
| 9 | | pccl 16887 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
| 10 | 9 | ancoms 458 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
| 11 | 10 | nn0zd 12639 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℤ) |
| 12 | | fznn 13632 |
. . . . . . . 8
⊢ ((𝑝 pCnt 𝐴) ∈ ℤ → (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)))) |
| 13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)))) |
| 14 | 13 | anbi2d 630 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))))) |
| 15 | | an12 645 |
. . . . . . 7
⊢ ((𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)))) |
| 16 | | prmz 16712 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℤ) |
| 18 | | iddvdsexp 16317 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℤ ∧ 𝑘 ∈ ℕ) → 𝑝 ∥ (𝑝↑𝑘)) |
| 19 | 17, 18 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∥ (𝑝↑𝑘)) |
| 20 | 16 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈
ℤ) |
| 21 | | prmnn 16711 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
| 23 | | nnnn0 12533 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
| 24 | | nnexpcl 14115 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑘) ∈
ℕ) |
| 25 | 22, 23, 24 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℕ) |
| 26 | 25 | nnzd 12640 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℤ) |
| 27 | | nnz 12634 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
| 28 | 27 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℤ) |
| 29 | | dvdstr 16331 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℤ ∧ (𝑝↑𝑘) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝑝 ∥ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ∥ 𝐴) → 𝑝 ∥ 𝐴)) |
| 30 | 20, 26, 28, 29 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∥ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ∥ 𝐴) → 𝑝 ∥ 𝐴)) |
| 31 | 19, 30 | mpand 695 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 → 𝑝 ∥ 𝐴)) |
| 32 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℕ) |
| 33 | | dvdsle 16347 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℕ) → (𝑝 ∥ 𝐴 → 𝑝 ≤ 𝐴)) |
| 34 | 20, 32, 33 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝 ∥ 𝐴 → 𝑝 ≤ 𝐴)) |
| 35 | 31, 34 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 → 𝑝 ≤ 𝐴)) |
| 36 | 21 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈
ℕ) |
| 37 | | fznn 13632 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ (1...𝐴) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝐴))) |
| 38 | 37 | baibd 539 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℕ) → (𝑝 ∈ (1...𝐴) ↔ 𝑝 ≤ 𝐴)) |
| 39 | 28, 36, 38 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝 ∈ (1...𝐴) ↔ 𝑝 ≤ 𝐴)) |
| 40 | 35, 39 | sylibrd 259 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 → 𝑝 ∈ (1...𝐴))) |
| 41 | 40 | pm4.71rd 562 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∥ 𝐴 ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝↑𝑘) ∥ 𝐴))) |
| 42 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑝↑𝑘) → (𝑥 ∥ 𝐴 ↔ (𝑝↑𝑘) ∥ 𝐴)) |
| 43 | 42 | elrab3 3693 |
. . . . . . . . . 10
⊢ ((𝑝↑𝑘) ∈ ℕ → ((𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ↔ (𝑝↑𝑘) ∥ 𝐴)) |
| 44 | 25, 43 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ↔ (𝑝↑𝑘) ∥ 𝐴)) |
| 45 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈
ℙ) |
| 46 | 23 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
ℕ0) |
| 47 | | pcdvdsb 16907 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝↑𝑘) ∥ 𝐴)) |
| 48 | 45, 28, 46, 47 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝↑𝑘) ∥ 𝐴)) |
| 49 | 48 | anbi2d 630 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝↑𝑘) ∥ 𝐴))) |
| 50 | 41, 44, 49 | 3bitr4rd 312 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)) ↔ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴})) |
| 51 | 50 | pm5.32da 579 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑘 ∈ ℕ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
| 52 | 15, 51 | bitrid 283 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
| 53 | 14, 52 | bitrd 279 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
| 54 | 53 | pm5.32da 579 |
. . . 4
⊢ (𝐴 ∈ ℕ → ((𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) ↔ (𝑝 ∈ ℙ ∧ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴})))) |
| 55 | | elin 3967 |
. . . . . 6
⊢ (𝑝 ∈ ((1...𝐴) ∩ ℙ) ↔ (𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ)) |
| 56 | 55 | anbi1i 624 |
. . . . 5
⊢ ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ ((𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) |
| 57 | | anass 468 |
. . . . 5
⊢ (((𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))))) |
| 58 | | an12 645 |
. . . . 5
⊢ ((𝑝 ∈ (1...𝐴) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) ↔ (𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))))) |
| 59 | 56, 57, 58 | 3bitri 297 |
. . . 4
⊢ ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))))) |
| 60 | | anass 468 |
. . . 4
⊢ (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) ↔ (𝑝 ∈ ℙ ∧ (𝑘 ∈ ℕ ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
| 61 | 54, 59, 60 | 3bitr4g 314 |
. . 3
⊢ (𝐴 ∈ ℕ → ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}))) |
| 62 | 4 | sselda 3983 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) → 𝑛 ∈ ℕ) |
| 63 | | vmacl 27161 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 64 | 62, 63 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) → (Λ‘𝑛) ∈ ℝ) |
| 65 | 64 | recnd 11289 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴}) → (Λ‘𝑛) ∈ ℂ) |
| 66 | | simprr 773 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ (𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0) |
| 67 | 1, 2, 4, 8, 61, 65, 66 | fsumvma 27257 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} (Λ‘𝑛) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘))) |
| 68 | | elinel2 4202 |
. . . . . . 7
⊢ (𝑝 ∈ ((1...𝐴) ∩ ℙ) → 𝑝 ∈ ℙ) |
| 69 | 68 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → 𝑝 ∈ ℙ) |
| 70 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) → 𝑘 ∈ ℕ) |
| 71 | 70 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → 𝑘 ∈ ℕ) |
| 72 | | vmappw 27159 |
. . . . . 6
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
| 73 | 69, 71, 72 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
| 74 | 73 | sumeq2dv 15738 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘)) = Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝)) |
| 75 | | fzfid 14014 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (1...(𝑝 pCnt 𝐴)) ∈ Fin) |
| 76 | 68, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝑝 ∈ ((1...𝐴) ∩ ℙ) → 𝑝 ∈ ℕ) |
| 77 | 76 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
| 78 | 77 | nnrpd 13075 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
| 79 | 78 | relogcld 26665 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
| 80 | 79 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
| 81 | | fsumconst 15826 |
. . . . 5
⊢
(((1...(𝑝 pCnt 𝐴)) ∈ Fin ∧
(log‘𝑝) ∈
ℂ) → Σ𝑘
∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝) = ((♯‘(1...(𝑝 pCnt 𝐴))) · (log‘𝑝))) |
| 82 | 75, 80, 81 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝) = ((♯‘(1...(𝑝 pCnt 𝐴))) · (log‘𝑝))) |
| 83 | 68, 10 | sylan2 593 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
| 84 | | hashfz1 14385 |
. . . . . 6
⊢ ((𝑝 pCnt 𝐴) ∈ ℕ0 →
(♯‘(1...(𝑝 pCnt
𝐴))) = (𝑝 pCnt 𝐴)) |
| 85 | 83, 84 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) →
(♯‘(1...(𝑝 pCnt
𝐴))) = (𝑝 pCnt 𝐴)) |
| 86 | 85 | oveq1d 7446 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) →
((♯‘(1...(𝑝
pCnt 𝐴))) ·
(log‘𝑝)) = ((𝑝 pCnt 𝐴) · (log‘𝑝))) |
| 87 | 74, 82, 86 | 3eqtrd 2781 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘)) = ((𝑝 pCnt 𝐴) · (log‘𝑝))) |
| 88 | 87 | sumeq2dv 15738 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝↑𝑘)) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝))) |
| 89 | | pclogsum 27259 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝)) = (log‘𝐴)) |
| 90 | 67, 88, 89 | 3eqtrd 2781 |
1
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴} (Λ‘𝑛) = (log‘𝐴)) |