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 \{x \in ℕ \| x ∥ A\}} Λ (n) = \log A$

Proof

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

Metamath Proof Explorer

Theorem vmasum

Proof