pclogsum

Description: The logarithmic analogue of pcprod . The sum of the logarithms of the primes dividing A multiplied by their powers yields the logarithm of A . (Contributed by Mario Carneiro, 15-Apr-2016)

		Ref	Expression
	Assertion	pclogsum	$⊢ A \in ℕ \to \sum_{p \in (1 \dots A) \cap ℙ} (p pCnt A) \log p = \log A$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ p \in ((1 \dots A) \cap ℙ) \leftrightarrow (p \in (1 \dots A) \land p \in ℙ)$
2	1	baib	$⊢ p \in (1 \dots A) \to (p \in ((1 \dots A) \cap ℙ) \leftrightarrow p \in ℙ)$
3	2	ifbid	$⊢ p \in (1 \dots A) \to if (p \in ((1 \dots A) \cap ℙ), \log p^{p pCnt A}, 0) = if (p \in ℙ, \log p^{p pCnt A}, 0)$
4		fvif	$⊢ \log if (p \in ℙ, p^{p pCnt A}, 1) = if (p \in ℙ, \log p^{p pCnt A}, \log 1)$
5		log1	$⊢ \log 1 = 0$
6		ifeq2	$⊢ \log 1 = 0 \to if (p \in ℙ, \log p^{p pCnt A}, \log 1) = if (p \in ℙ, \log p^{p pCnt A}, 0)$
7	5 6	ax-mp	$⊢ if (p \in ℙ, \log p^{p pCnt A}, \log 1) = if (p \in ℙ, \log p^{p pCnt A}, 0)$
8	4 7	eqtri	$⊢ \log if (p \in ℙ, p^{p pCnt A}, 1) = if (p \in ℙ, \log p^{p pCnt A}, 0)$
9	3 8	eqtr4di	$⊢ p \in (1 \dots A) \to if (p \in ((1 \dots A) \cap ℙ), \log p^{p pCnt A}, 0) = \log if (p \in ℙ, p^{p pCnt A}, 1)$
10	9	sumeq2i	$⊢ \sum_{p = 1}^{A} if (p \in ((1 \dots A) \cap ℙ), \log p^{p pCnt A}, 0) = \sum_{p = 1}^{A} \log if (p \in ℙ, p^{p pCnt A}, 1)$
11		inss1	$⊢ (1 \dots A) \cap ℙ \subseteq (1 \dots A)$
12		simpr	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p \in ((1 \dots A) \cap ℙ)$
13	12	elin1d	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p \in (1 \dots A)$
14		elfznn	$⊢ p \in (1 \dots A) \to p \in ℕ$
15	13 14	syl	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p \in ℕ$
16	12	elin2d	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p \in ℙ$
17		simpl	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to A \in ℕ$
18	16 17	pccld	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p pCnt A \in ℕ_{0}$
19	15 18	nnexpcld	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p^{p pCnt A} \in ℕ$
20	19	nnrpd	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p^{p pCnt A} \in ℝ^{+}$
21	20	relogcld	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to \log p^{p pCnt A} \in ℝ$
22	21	recnd	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to \log p^{p pCnt A} \in ℂ$
23	22	ralrimiva	$⊢ A \in ℕ \to \forall p \in ((1 \dots A) \cap ℙ) \log p^{p pCnt A} \in ℂ$
24		fzfi	$⊢ (1 \dots A) \in Fin$
25	24	olci	$⊢ ((1 \dots A) \subseteq ℤ_{\geq 1} \lor (1 \dots A) \in Fin)$
26		sumss2	$⊢ (((1 \dots A) \cap ℙ \subseteq (1 \dots A) \land \forall p \in ((1 \dots A) \cap ℙ) \log p^{p pCnt A} \in ℂ) \land ((1 \dots A) \subseteq ℤ_{\geq 1} \lor (1 \dots A) \in Fin)) \to \sum_{p \in (1 \dots A) \cap ℙ} \log p^{p pCnt A} = \sum_{p = 1}^{A} if (p \in ((1 \dots A) \cap ℙ), \log p^{p pCnt A}, 0)$
27	25 26	mpan2	$⊢ ((1 \dots A) \cap ℙ \subseteq (1 \dots A) \land \forall p \in ((1 \dots A) \cap ℙ) \log p^{p pCnt A} \in ℂ) \to \sum_{p \in (1 \dots A) \cap ℙ} \log p^{p pCnt A} = \sum_{p = 1}^{A} if (p \in ((1 \dots A) \cap ℙ), \log p^{p pCnt A}, 0)$
28	11 23 27	sylancr	$⊢ A \in ℕ \to \sum_{p \in (1 \dots A) \cap ℙ} \log p^{p pCnt A} = \sum_{p = 1}^{A} if (p \in ((1 \dots A) \cap ℙ), \log p^{p pCnt A}, 0)$
29	15	nnrpd	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p \in ℝ^{+}$
30	18	nn0zd	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to p pCnt A \in ℤ$
31		relogexp	$⊢ (p \in ℝ^{+} \land p pCnt A \in ℤ) \to \log p^{p pCnt A} = (p pCnt A) \log p$
32	29 30 31	syl2anc	$⊢ (A \in ℕ \land p \in ((1 \dots A) \cap ℙ)) \to \log p^{p pCnt A} = (p pCnt A) \log p$
33	32	sumeq2dv	$⊢ A \in ℕ \to \sum_{p \in (1 \dots A) \cap ℙ} \log p^{p pCnt A} = \sum_{p \in (1 \dots A) \cap ℙ} (p pCnt A) \log p$
34	28 33	eqtr3d	$⊢ A \in ℕ \to \sum_{p = 1}^{A} if (p \in ((1 \dots A) \cap ℙ), \log p^{p pCnt A}, 0) = \sum_{p \in (1 \dots A) \cap ℙ} (p pCnt A) \log p$
35	14	adantl	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to p \in ℕ$
36		eleq1w	$⊢ n = p \to (n \in ℙ \leftrightarrow p \in ℙ)$
37		id	$⊢ n = p \to n = p$
38		oveq1	$⊢ n = p \to n pCnt A = p pCnt A$
39	37 38	oveq12d	$⊢ n = p \to n^{n pCnt A} = p^{p pCnt A}$
40	36 39	ifbieq1d	$⊢ n = p \to if (n \in ℙ, n^{n pCnt A}, 1) = if (p \in ℙ, p^{p pCnt A}, 1)$
41	40	fveq2d	$⊢ n = p \to \log if (n \in ℙ, n^{n pCnt A}, 1) = \log if (p \in ℙ, p^{p pCnt A}, 1)$
42		eqid	$⊢ (n \in ℕ ⟼ \log if (n \in ℙ, n^{n pCnt A}, 1)) = (n \in ℕ ⟼ \log if (n \in ℙ, n^{n pCnt A}, 1))$
43		fvex	$⊢ \log if (p \in ℙ, p^{p pCnt A}, 1) \in V$
44	41 42 43	fvmpt	$⊢ p \in ℕ \to (n \in ℕ ⟼ \log if (n \in ℙ, n^{n pCnt A}, 1)) (p) = \log if (p \in ℙ, p^{p pCnt A}, 1)$
45	35 44	syl	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to (n \in ℕ ⟼ \log if (n \in ℙ, n^{n pCnt A}, 1)) (p) = \log if (p \in ℙ, p^{p pCnt A}, 1)$
46		elnnuz	$⊢ A \in ℕ \leftrightarrow A \in ℤ_{\geq 1}$
47	46	biimpi	$⊢ A \in ℕ \to A \in ℤ_{\geq 1}$
48	35	adantr	$⊢ ((A \in ℕ \land p \in (1 \dots A)) \land p \in ℙ) \to p \in ℕ$
49		simpr	$⊢ ((A \in ℕ \land p \in (1 \dots A)) \land p \in ℙ) \to p \in ℙ$
50		simpll	$⊢ ((A \in ℕ \land p \in (1 \dots A)) \land p \in ℙ) \to A \in ℕ$
51	49 50	pccld	$⊢ ((A \in ℕ \land p \in (1 \dots A)) \land p \in ℙ) \to p pCnt A \in ℕ_{0}$
52	48 51	nnexpcld	$⊢ ((A \in ℕ \land p \in (1 \dots A)) \land p \in ℙ) \to p^{p pCnt A} \in ℕ$
53		1nn	$⊢ 1 \in ℕ$
54	53	a1i	$⊢ ((A \in ℕ \land p \in (1 \dots A)) \land \neg p \in ℙ) \to 1 \in ℕ$
55	52 54	ifclda	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to if (p \in ℙ, p^{p pCnt A}, 1) \in ℕ$
56	55	nnrpd	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to if (p \in ℙ, p^{p pCnt A}, 1) \in ℝ^{+}$
57	56	relogcld	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to \log if (p \in ℙ, p^{p pCnt A}, 1) \in ℝ$
58	57	recnd	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to \log if (p \in ℙ, p^{p pCnt A}, 1) \in ℂ$
59	45 47 58	fsumser	$⊢ A \in ℕ \to \sum_{p = 1}^{A} \log if (p \in ℙ, p^{p pCnt A}, 1) = seq 1 (+ (n \in ℕ ⟼ \log if (n \in ℙ, n^{n pCnt A}, 1))) (A)$
60		rpmulcl	$⊢ (p \in ℝ^{+} \land m \in ℝ^{+}) \to p m \in ℝ^{+}$
61	60	adantl	$⊢ (A \in ℕ \land (p \in ℝ^{+} \land m \in ℝ^{+})) \to p m \in ℝ^{+}$
62		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1))$
63		ovex	$⊢ p^{p pCnt A} \in V$
64		1ex	$⊢ 1 \in V$
65	63 64	ifex	$⊢ if (p \in ℙ, p^{p pCnt A}, 1) \in V$
66	40 62 65	fvmpt	$⊢ p \in ℕ \to (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1)) (p) = if (p \in ℙ, p^{p pCnt A}, 1)$
67	35 66	syl	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1)) (p) = if (p \in ℙ, p^{p pCnt A}, 1)$
68	67 56	eqeltrd	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1)) (p) \in ℝ^{+}$
69		relogmul	$⊢ (p \in ℝ^{+} \land m \in ℝ^{+}) \to \log p m = \log p + \log m$
70	69	adantl	$⊢ (A \in ℕ \land (p \in ℝ^{+} \land m \in ℝ^{+})) \to \log p m = \log p + \log m$
71	67	fveq2d	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to \log (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1)) (p) = \log if (p \in ℙ, p^{p pCnt A}, 1)$
72	71 45	eqtr4d	$⊢ (A \in ℕ \land p \in (1 \dots A)) \to \log (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1)) (p) = (n \in ℕ ⟼ \log if (n \in ℙ, n^{n pCnt A}, 1)) (p)$
73	61 68 47 70 72	seqhomo	$⊢ A \in ℕ \to \log seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1))) (A) = seq 1 (+ (n \in ℕ ⟼ \log if (n \in ℙ, n^{n pCnt A}, 1))) (A)$
74	62	pcprod	$⊢ A \in ℕ \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1))) (A) = A$
75	74	fveq2d	$⊢ A \in ℕ \to \log seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt A}, 1))) (A) = \log A$
76	59 73 75	3eqtr2d	$⊢ A \in ℕ \to \sum_{p = 1}^{A} \log if (p \in ℙ, p^{p pCnt A}, 1) = \log A$
77	10 34 76	3eqtr3a	$⊢ A \in ℕ \to \sum_{p \in (1 \dots A) \cap ℙ} (p pCnt A) \log p = \log A$

Metamath Proof Explorer

Theorem pclogsum

Proof