sgmppw

Description: The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016)

		Ref	Expression
	Assertion	sgmppw	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to A σ P^{N} = \sum_{k = 0}^{N} {(P^{A})}^{k}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to A \in ℂ$
2		simp2	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to P \in ℙ$
3		prmnn	$⊢ P \in ℙ \to P \in ℕ$
4	2 3	syl	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to P \in ℕ$
5		simp3	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
6	4 5	nnexpcld	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to P^{N} \in ℕ$
7		sgmval	$⊢ (A \in ℂ \land P^{N} \in ℕ) \to A σ P^{N} = \sum_{n \in \{x \in ℕ \| x ∥ P^{N}\}} n^{A}$
8	1 6 7	syl2anc	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to A σ P^{N} = \sum_{n \in \{x \in ℕ \| x ∥ P^{N}\}} n^{A}$
9		oveq1	$⊢ n = P^{k} \to n^{A} = {(P^{k})}^{A}$
10		fzfid	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to (0 \dots N) \in Fin$
11		eqid	$⊢ (i \in (0 \dots N) ⟼ P^{i}) = (i \in (0 \dots N) ⟼ P^{i})$
12	11	dvdsppwf1o	$⊢ (P \in ℙ \land N \in ℕ_{0}) \to (i \in (0 \dots N) ⟼ P^{i}) : (0 \dots N) \underset{1-1 onto}{⟶} \{x \in ℕ \| x ∥ P^{N}\}$
13	2 5 12	syl2anc	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to (i \in (0 \dots N) ⟼ P^{i}) : (0 \dots N) \underset{1-1 onto}{⟶} \{x \in ℕ \| x ∥ P^{N}\}$
14		oveq2	$⊢ i = k \to P^{i} = P^{k}$
15		ovex	$⊢ P^{k} \in V$
16	14 11 15	fvmpt	$⊢ k \in (0 \dots N) \to (i \in (0 \dots N) ⟼ P^{i}) (k) = P^{k}$
17	16	adantl	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to (i \in (0 \dots N) ⟼ P^{i}) (k) = P^{k}$
18		elrabi	$⊢ n \in \{x \in ℕ \| x ∥ P^{N}\} \to n \in ℕ$
19	18	nncnd	$⊢ n \in \{x \in ℕ \| x ∥ P^{N}\} \to n \in ℂ$
20		cxpcl	$⊢ (n \in ℂ \land A \in ℂ) \to n^{A} \in ℂ$
21	19 1 20	syl2anr	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land n \in \{x \in ℕ \| x ∥ P^{N}\}) \to n^{A} \in ℂ$
22	9 10 13 17 21	fsumf1o	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to \sum_{n \in \{x \in ℕ \| x ∥ P^{N}\}} n^{A} = \sum_{k = 0}^{N} {(P^{k})}^{A}$
23		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
24	23	adantl	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to k \in ℕ_{0}$
25	24	nn0cnd	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to k \in ℂ$
26	1	adantr	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to A \in ℂ$
27	25 26	mulcomd	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to k A = A k$
28	27	oveq2d	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P^{k A} = P^{A k}$
29	4	adantr	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P \in ℕ$
30	29	nnrpd	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P \in ℝ^{+}$
31	24	nn0red	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to k \in ℝ$
32	30 31 26	cxpmuld	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P^{k A} = {(P^{k})}^{A}$
33	29	nncnd	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P \in ℂ$
34		cxpexp	$⊢ (P \in ℂ \land k \in ℕ_{0}) \to P^{k} = P^{k}$
35	33 24 34	syl2anc	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P^{k} = P^{k}$
36	35	oveq1d	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to {(P^{k})}^{A} = {(P^{k})}^{A}$
37	32 36	eqtrd	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P^{k A} = {(P^{k})}^{A}$
38	33 26 24	cxpmul2d	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to P^{A k} = {(P^{A})}^{k}$
39	28 37 38	3eqtr3d	$⊢ ((A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to {(P^{k})}^{A} = {(P^{A})}^{k}$
40	39	sumeq2dv	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to \sum_{k = 0}^{N} {(P^{k})}^{A} = \sum_{k = 0}^{N} {(P^{A})}^{k}$
41	8 22 40	3eqtrd	$⊢ (A \in ℂ \land P \in ℙ \land N \in ℕ_{0}) \to A σ P^{N} = \sum_{k = 0}^{N} {(P^{A})}^{k}$

Metamath Proof Explorer

Theorem sgmppw

Proof