# 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 ${⊢}{A}\in ℕ\to \sum _{{n}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}}\Lambda \left({n}\right)=\mathrm{log}{A}$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{n}={{p}}^{{k}}\to \Lambda \left({n}\right)=\Lambda \left({{p}}^{{k}}\right)$
2 fzfid ${⊢}{A}\in ℕ\to \left(1\dots {A}\right)\in \mathrm{Fin}$
3 dvdsssfz1 ${⊢}{A}\in ℕ\to \left\{{x}\in ℕ|{x}\parallel {A}\right\}\subseteq \left(1\dots {A}\right)$
4 2 3 ssfid ${⊢}{A}\in ℕ\to \left\{{x}\in ℕ|{x}\parallel {A}\right\}\in \mathrm{Fin}$
5 ssrab2 ${⊢}\left\{{x}\in ℕ|{x}\parallel {A}\right\}\subseteq ℕ$
6 5 a1i ${⊢}{A}\in ℕ\to \left\{{x}\in ℕ|{x}\parallel {A}\right\}\subseteq ℕ$
7 inss1 ${⊢}\left(1\dots {A}\right)\cap ℙ\subseteq \left(1\dots {A}\right)$
8 ssfi ${⊢}\left(\left(1\dots {A}\right)\in \mathrm{Fin}\wedge \left(1\dots {A}\right)\cap ℙ\subseteq \left(1\dots {A}\right)\right)\to \left(1\dots {A}\right)\cap ℙ\in \mathrm{Fin}$
9 2 7 8 sylancl ${⊢}{A}\in ℕ\to \left(1\dots {A}\right)\cap ℙ\in \mathrm{Fin}$
10 pccl ${⊢}\left({p}\in ℙ\wedge {A}\in ℕ\right)\to {p}\mathrm{pCnt}{A}\in {ℕ}_{0}$
11 10 ancoms ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to {p}\mathrm{pCnt}{A}\in {ℕ}_{0}$
12 11 nn0zd ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to {p}\mathrm{pCnt}{A}\in ℤ$
13 fznn ${⊢}{p}\mathrm{pCnt}{A}\in ℤ\to \left({k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)↔\left({k}\in ℕ\wedge {k}\le {p}\mathrm{pCnt}{A}\right)\right)$
14 12 13 syl ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left({k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)↔\left({k}\in ℕ\wedge {k}\le {p}\mathrm{pCnt}{A}\right)\right)$
15 14 anbi2d ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\left({p}\in \left(1\dots {A}\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)↔\left({p}\in \left(1\dots {A}\right)\wedge \left({k}\in ℕ\wedge {k}\le {p}\mathrm{pCnt}{A}\right)\right)\right)$
16 an12 ${⊢}\left({p}\in \left(1\dots {A}\right)\wedge \left({k}\in ℕ\wedge {k}\le {p}\mathrm{pCnt}{A}\right)\right)↔\left({k}\in ℕ\wedge \left({p}\in \left(1\dots {A}\right)\wedge {k}\le {p}\mathrm{pCnt}{A}\right)\right)$
17 prmz ${⊢}{p}\in ℙ\to {p}\in ℤ$
18 17 adantl ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to {p}\in ℤ$
19 iddvdsexp ${⊢}\left({p}\in ℤ\wedge {k}\in ℕ\right)\to {p}\parallel {{p}}^{{k}}$
20 18 19 sylan ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {p}\parallel {{p}}^{{k}}$
21 17 ad2antlr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {p}\in ℤ$
22 prmnn ${⊢}{p}\in ℙ\to {p}\in ℕ$
23 22 adantl ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to {p}\in ℕ$
24 nnnn0 ${⊢}{k}\in ℕ\to {k}\in {ℕ}_{0}$
25 nnexpcl ${⊢}\left({p}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\to {{p}}^{{k}}\in ℕ$
26 23 24 25 syl2an ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {{p}}^{{k}}\in ℕ$
27 26 nnzd ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {{p}}^{{k}}\in ℤ$
28 nnz ${⊢}{A}\in ℕ\to {A}\in ℤ$
29 28 ad2antrr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {A}\in ℤ$
30 dvdstr ${⊢}\left({p}\in ℤ\wedge {{p}}^{{k}}\in ℤ\wedge {A}\in ℤ\right)\to \left(\left({p}\parallel {{p}}^{{k}}\wedge {{p}}^{{k}}\parallel {A}\right)\to {p}\parallel {A}\right)$
31 21 27 29 30 syl3anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left(\left({p}\parallel {{p}}^{{k}}\wedge {{p}}^{{k}}\parallel {A}\right)\to {p}\parallel {A}\right)$
32 20 31 mpand ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({{p}}^{{k}}\parallel {A}\to {p}\parallel {A}\right)$
33 simpll ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {A}\in ℕ$
34 dvdsle ${⊢}\left({p}\in ℤ\wedge {A}\in ℕ\right)\to \left({p}\parallel {A}\to {p}\le {A}\right)$
35 21 33 34 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({p}\parallel {A}\to {p}\le {A}\right)$
36 32 35 syld ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({{p}}^{{k}}\parallel {A}\to {p}\le {A}\right)$
37 22 ad2antlr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {p}\in ℕ$
38 fznn ${⊢}{A}\in ℤ\to \left({p}\in \left(1\dots {A}\right)↔\left({p}\in ℕ\wedge {p}\le {A}\right)\right)$
39 38 baibd ${⊢}\left({A}\in ℤ\wedge {p}\in ℕ\right)\to \left({p}\in \left(1\dots {A}\right)↔{p}\le {A}\right)$
40 29 37 39 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({p}\in \left(1\dots {A}\right)↔{p}\le {A}\right)$
41 36 40 sylibrd ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({{p}}^{{k}}\parallel {A}\to {p}\in \left(1\dots {A}\right)\right)$
42 41 pm4.71rd ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({{p}}^{{k}}\parallel {A}↔\left({p}\in \left(1\dots {A}\right)\wedge {{p}}^{{k}}\parallel {A}\right)\right)$
43 breq1 ${⊢}{x}={{p}}^{{k}}\to \left({x}\parallel {A}↔{{p}}^{{k}}\parallel {A}\right)$
44 43 elrab3 ${⊢}{{p}}^{{k}}\in ℕ\to \left({{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}↔{{p}}^{{k}}\parallel {A}\right)$
45 26 44 syl ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}↔{{p}}^{{k}}\parallel {A}\right)$
46 simplr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {p}\in ℙ$
47 24 adantl ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}\in {ℕ}_{0}$
48 pcdvdsb ${⊢}\left({p}\in ℙ\wedge {A}\in ℤ\wedge {k}\in {ℕ}_{0}\right)\to \left({k}\le {p}\mathrm{pCnt}{A}↔{{p}}^{{k}}\parallel {A}\right)$
49 46 29 47 48 syl3anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({k}\le {p}\mathrm{pCnt}{A}↔{{p}}^{{k}}\parallel {A}\right)$
50 49 anbi2d ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left(\left({p}\in \left(1\dots {A}\right)\wedge {k}\le {p}\mathrm{pCnt}{A}\right)↔\left({p}\in \left(1\dots {A}\right)\wedge {{p}}^{{k}}\parallel {A}\right)\right)$
51 42 45 50 3bitr4rd ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left(\left({p}\in \left(1\dots {A}\right)\wedge {k}\le {p}\mathrm{pCnt}{A}\right)↔{{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)$
52 51 pm5.32da ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\left({k}\in ℕ\wedge \left({p}\in \left(1\dots {A}\right)\wedge {k}\le {p}\mathrm{pCnt}{A}\right)\right)↔\left({k}\in ℕ\wedge {{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\right)$
53 16 52 syl5bb ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\left({p}\in \left(1\dots {A}\right)\wedge \left({k}\in ℕ\wedge {k}\le {p}\mathrm{pCnt}{A}\right)\right)↔\left({k}\in ℕ\wedge {{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\right)$
54 15 53 bitrd ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\left({p}\in \left(1\dots {A}\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)↔\left({k}\in ℕ\wedge {{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\right)$
55 54 pm5.32da ${⊢}{A}\in ℕ\to \left(\left({p}\in ℙ\wedge \left({p}\in \left(1\dots {A}\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\right)↔\left({p}\in ℙ\wedge \left({k}\in ℕ\wedge {{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\right)\right)$
56 elin ${⊢}{p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)↔\left({p}\in \left(1\dots {A}\right)\wedge {p}\in ℙ\right)$
57 56 anbi1i ${⊢}\left({p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)↔\left(\left({p}\in \left(1\dots {A}\right)\wedge {p}\in ℙ\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)$
58 anass ${⊢}\left(\left({p}\in \left(1\dots {A}\right)\wedge {p}\in ℙ\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)↔\left({p}\in \left(1\dots {A}\right)\wedge \left({p}\in ℙ\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\right)$
59 an12 ${⊢}\left({p}\in \left(1\dots {A}\right)\wedge \left({p}\in ℙ\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\right)↔\left({p}\in ℙ\wedge \left({p}\in \left(1\dots {A}\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\right)$
60 57 58 59 3bitri ${⊢}\left({p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)↔\left({p}\in ℙ\wedge \left({p}\in \left(1\dots {A}\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\right)$
61 anass ${⊢}\left(\left({p}\in ℙ\wedge {k}\in ℕ\right)\wedge {{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)↔\left({p}\in ℙ\wedge \left({k}\in ℕ\wedge {{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\right)$
62 55 60 61 3bitr4g ${⊢}{A}\in ℕ\to \left(\left({p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)↔\left(\left({p}\in ℙ\wedge {k}\in ℕ\right)\wedge {{p}}^{{k}}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\right)$
63 6 sselda ${⊢}\left({A}\in ℕ\wedge {n}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\to {n}\in ℕ$
64 vmacl ${⊢}{n}\in ℕ\to \Lambda \left({n}\right)\in ℝ$
65 63 64 syl ${⊢}\left({A}\in ℕ\wedge {n}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\to \Lambda \left({n}\right)\in ℝ$
66 65 recnd ${⊢}\left({A}\in ℕ\wedge {n}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\right)\to \Lambda \left({n}\right)\in ℂ$
67 simprr ${⊢}\left({A}\in ℕ\wedge \left({n}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}\wedge \Lambda \left({n}\right)=0\right)\right)\to \Lambda \left({n}\right)=0$
68 1 4 6 9 62 66 67 fsumvma ${⊢}{A}\in ℕ\to \sum _{{n}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}}\Lambda \left({n}\right)=\sum _{{p}\in \left(1\dots {A}\right)\cap ℙ}\sum _{{k}=1}^{{p}\mathrm{pCnt}{A}}\Lambda \left({{p}}^{{k}}\right)$
69 elinel2 ${⊢}{p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\to {p}\in ℙ$
70 69 ad2antlr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\to {p}\in ℙ$
71 elfznn ${⊢}{k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\to {k}\in ℕ$
72 71 adantl ${⊢}\left(\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\to {k}\in ℕ$
73 vmappw ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \Lambda \left({{p}}^{{k}}\right)=\mathrm{log}{p}$
74 70 72 73 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\wedge {k}\in \left(1\dots {p}\mathrm{pCnt}{A}\right)\right)\to \Lambda \left({{p}}^{{k}}\right)=\mathrm{log}{p}$
75 74 sumeq2dv ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \sum _{{k}=1}^{{p}\mathrm{pCnt}{A}}\Lambda \left({{p}}^{{k}}\right)=\sum _{{k}=1}^{{p}\mathrm{pCnt}{A}}\mathrm{log}{p}$
76 fzfid ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \left(1\dots {p}\mathrm{pCnt}{A}\right)\in \mathrm{Fin}$
77 69 22 syl ${⊢}{p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\to {p}\in ℕ$
78 77 adantl ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to {p}\in ℕ$
79 78 nnrpd ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to {p}\in {ℝ}^{+}$
80 79 relogcld ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \mathrm{log}{p}\in ℝ$
81 80 recnd ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \mathrm{log}{p}\in ℂ$
82 fsumconst ${⊢}\left(\left(1\dots {p}\mathrm{pCnt}{A}\right)\in \mathrm{Fin}\wedge \mathrm{log}{p}\in ℂ\right)\to \sum _{{k}=1}^{{p}\mathrm{pCnt}{A}}\mathrm{log}{p}=\left|\left(1\dots {p}\mathrm{pCnt}{A}\right)\right|\mathrm{log}{p}$
83 76 81 82 syl2anc ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \sum _{{k}=1}^{{p}\mathrm{pCnt}{A}}\mathrm{log}{p}=\left|\left(1\dots {p}\mathrm{pCnt}{A}\right)\right|\mathrm{log}{p}$
84 69 11 sylan2 ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to {p}\mathrm{pCnt}{A}\in {ℕ}_{0}$
85 hashfz1 ${⊢}{p}\mathrm{pCnt}{A}\in {ℕ}_{0}\to \left|\left(1\dots {p}\mathrm{pCnt}{A}\right)\right|={p}\mathrm{pCnt}{A}$
86 84 85 syl ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \left|\left(1\dots {p}\mathrm{pCnt}{A}\right)\right|={p}\mathrm{pCnt}{A}$
87 86 oveq1d ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \left|\left(1\dots {p}\mathrm{pCnt}{A}\right)\right|\mathrm{log}{p}=\left({p}\mathrm{pCnt}{A}\right)\mathrm{log}{p}$
88 75 83 87 3eqtrd ${⊢}\left({A}\in ℕ\wedge {p}\in \left(\left(1\dots {A}\right)\cap ℙ\right)\right)\to \sum _{{k}=1}^{{p}\mathrm{pCnt}{A}}\Lambda \left({{p}}^{{k}}\right)=\left({p}\mathrm{pCnt}{A}\right)\mathrm{log}{p}$
89 88 sumeq2dv ${⊢}{A}\in ℕ\to \sum _{{p}\in \left(1\dots {A}\right)\cap ℙ}\sum _{{k}=1}^{{p}\mathrm{pCnt}{A}}\Lambda \left({{p}}^{{k}}\right)=\sum _{{p}\in \left(1\dots {A}\right)\cap ℙ}\left({p}\mathrm{pCnt}{A}\right)\mathrm{log}{p}$
90 pclogsum ${⊢}{A}\in ℕ\to \sum _{{p}\in \left(1\dots {A}\right)\cap ℙ}\left({p}\mathrm{pCnt}{A}\right)\mathrm{log}{p}=\mathrm{log}{A}$
91 68 89 90 3eqtrd ${⊢}{A}\in ℕ\to \sum _{{n}\in \left\{{x}\in ℕ|{x}\parallel {A}\right\}}\Lambda \left({n}\right)=\mathrm{log}{A}$