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

Metamath Proof Explorer

Theorem vmasum

Proof