Metamath Proof Explorer

Theorem vmasum

Description: The sum of the von Mangoldt function over the divisors of n . Equation 9.2.4 of Shapiro, p. 328 and theorem 2.10 in ApostolNT p. 32. (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Assertion vmasum ( 𝐴 ∈ ℕ → Σ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ( Λ ‘ 𝑛 ) = ( log ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝑛 ) = ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
2 dvdsfi ⊢ ( 𝐴 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ∈ Fin )
3 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ⊆ ℕ
4 3 a1i ⊢ ( 𝐴 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ⊆ ℕ )
5 fzfid ⊢ ( 𝐴 ∈ ℕ → ( 1 ... 𝐴 ) ∈ Fin )
6 inss1 ⊢ ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 )
7 ssfi ⊢ ( ( ( 1 ... 𝐴 ) ∈ Fin ∧ ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 ) ) → ( ( 1 ... 𝐴 ) ∩ ℙ ) ∈ Fin )
8 5 6 7 sylancl ⊢ ( 𝐴 ∈ ℕ → ( ( 1 ... 𝐴 ) ∩ ℙ ) ∈ Fin )
9 pccl ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
10 9 ancoms ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
11 10 nn0zd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℤ )
12 fznn ⊢ ( ( 𝑝 pCnt 𝐴 ) ∈ ℤ → ( 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ) )
13 11 12 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ) )
14 13 anbi2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ) ) )
15 an12 ⊢ ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ) )
16 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
17 16 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
18 iddvdsexp ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → 𝑝 ∥ ( 𝑝 ↑ 𝑘 ) )
19 17 18 sylan ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∥ ( 𝑝 ↑ 𝑘 ) )
20 16 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℤ )
21 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
22 21 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℕ )
23 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
24 nnexpcl ⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
25 22 23 24 syl2an ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
26 25 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
27 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
28 27 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℤ )
29 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝑝 ∥ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) → 𝑝 ∥ 𝐴 ) )
30 20 26 28 29 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ∥ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) → 𝑝 ∥ 𝐴 ) )
31 19 30 mpand ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 → 𝑝 ∥ 𝐴 ) )
32 simpll ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℕ )
33 dvdsle ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( 𝑝 ∥ 𝐴 → 𝑝 ≤ 𝐴 ) )
34 20 32 33 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ∥ 𝐴 → 𝑝 ≤ 𝐴 ) )
35 31 34 syld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 → 𝑝 ≤ 𝐴 ) )
36 21 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℕ )
37 fznn ⊢ ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( 1 ... 𝐴 ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝐴 ) ) )
38 37 baibd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ℕ ) → ( 𝑝 ∈ ( 1 ... 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
39 28 36 38 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ∈ ( 1 ... 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
40 35 39 sylibrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 → 𝑝 ∈ ( 1 ... 𝐴 ) ) )
41 40 pm4.71rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ↔ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) ) )
42 breq1 ⊢ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) → ( 𝑥 ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) )
43 42 elrab3 ⊢ ( ( 𝑝 ↑ 𝑘 ) ∈ ℕ → ( ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ↔ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) )
44 25 43 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ↔ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) )
45 simplr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℙ )
46 23 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
47 pcdvdsb ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) )
48 45 28 46 47 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) )
49 48 anbi2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ↔ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ ( 𝑝 ↑ 𝑘 ) ∥ 𝐴 ) ) )
50 41 44 49 3bitr4rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ↔ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) )
51 50 pm5.32da ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑘 ∈ ℕ ∧ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) ) )
52 15 51 bitrid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) ) )
53 14 52 bitrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) ) )
54 53 pm5.32da ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑝 ∈ ℙ ∧ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ) ↔ ( 𝑝 ∈ ℙ ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) ) ) )
55 elin ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑝 ∈ ℙ ) )
56 55 anbi1i ⊢ ( ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) )
57 anass ⊢ ( ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ) )
58 an12 ⊢ ( ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ) ↔ ( 𝑝 ∈ ℙ ∧ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ) )
59 56 57 58 3bitri ⊢ ( ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( 𝑝 ∈ ℙ ∧ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ) )
60 anass ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) ↔ ( 𝑝 ∈ ℙ ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) ) )
61 54 59 60 3bitr4g ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) ) )
62 4 sselda ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) → 𝑛 ∈ ℕ )
63 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
64 62 63 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
65 64 recnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
66 simprr ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( Λ ‘ 𝑛 ) = 0 )
67 1 2 4 8 61 65 66 fsumvma ⊢ ( 𝐴 ∈ ℕ → Σ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ( Λ ‘ 𝑛 ) = Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
68 elinel2 ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ℙ )
69 68 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) → 𝑝 ∈ ℙ )
70 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) → 𝑘 ∈ ℕ )
71 70 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) → 𝑘 ∈ ℕ )
72 vmappw ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
73 69 71 72 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
74 73 sumeq2dv ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ( log ‘ 𝑝 ) )
75 fzfid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ∈ Fin )
76 68 21 syl ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ℕ )
77 76 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
78 77 nnrpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
79 78 relogcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
80 79 recnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
81 fsumconst ⊢ ( ( ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ∈ Fin ∧ ( log ‘ 𝑝 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) · ( log ‘ 𝑝 ) ) )
82 75 80 81 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) · ( log ‘ 𝑝 ) ) )
83 68 10 sylan2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
84 hashfz1 ⊢ ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) = ( 𝑝 pCnt 𝐴 ) )
85 83 84 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) = ( 𝑝 pCnt 𝐴 ) )
86 85 oveq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( ( ♯ ‘ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ) · ( log ‘ 𝑝 ) ) = ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) )
87 74 82 86 3eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) )
88 87 sumeq2dv ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( 𝑝 pCnt 𝐴 ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) )
89 pclogsum ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) = ( log ‘ 𝐴 ) )
90 67 88 89 3eqtrd ⊢ ( 𝐴 ∈ ℕ → Σ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐴 } ( Λ ‘ 𝑛 ) = ( log ‘ 𝐴 ) )