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