Theorem sgmppw

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

	Ref	Expression
Assertion	sgmppw	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 σ ( 𝑃 ↑ 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑃 ↑𝑐 𝐴 ) ↑ 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
2		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → 𝑃 ∈ ℙ )
3		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
4	2 3	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → 𝑃 ∈ ℕ )
5		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
6	4 5	nnexpcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑁 ) ∈ ℕ )
7		sgmval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ↑ 𝑁 ) ∈ ℕ ) → ( 𝐴 σ ( 𝑃 ↑ 𝑁 ) ) = Σ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } ( 𝑛 ↑𝑐 𝐴 ) )
8	1 6 7	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 σ ( 𝑃 ↑ 𝑁 ) ) = Σ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } ( 𝑛 ↑𝑐 𝐴 ) )
9		oveq1	⊢ ( 𝑛 = ( 𝑃 ↑ 𝑘 ) → ( 𝑛 ↑𝑐 𝐴 ) = ( ( 𝑃 ↑ 𝑘 ) ↑𝑐 𝐴 ) )
10		fzfid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ... 𝑁 ) ∈ Fin )
11		eqid	⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ↑ 𝑖 ) ) = ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ↑ 𝑖 ) )
12	11	dvdsppwf1o	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ↑ 𝑖 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } )
13	2 5 12	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ↑ 𝑖 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } )
14		oveq2	⊢ ( 𝑖 = 𝑘 → ( 𝑃 ↑ 𝑖 ) = ( 𝑃 ↑ 𝑘 ) )
15		ovex	⊢ ( 𝑃 ↑ 𝑘 ) ∈ V
16	14 11 15	fvmpt	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ↑ 𝑖 ) ) ‘ 𝑘 ) = ( 𝑃 ↑ 𝑘 ) )
17	16	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑃 ↑ 𝑖 ) ) ‘ 𝑘 ) = ( 𝑃 ↑ 𝑘 ) )
18		elrabi	⊢ ( 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } → 𝑛 ∈ ℕ )
19	18	nncnd	⊢ ( 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } → 𝑛 ∈ ℂ )
20		cxpcl	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑛 ↑𝑐 𝐴 ) ∈ ℂ )
21	19 1 20	syl2anr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } ) → ( 𝑛 ↑𝑐 𝐴 ) ∈ ℂ )
22	9 10 13 17 21	fsumf1o	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑛 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝑁 ) } ( 𝑛 ↑𝑐 𝐴 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑃 ↑ 𝑘 ) ↑𝑐 𝐴 ) )
23		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
24	23	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
25	24	nn0cnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
26	1	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
27	25 26	mulcomd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑘 · 𝐴 ) = ( 𝐴 · 𝑘 ) )
28	27	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ↑𝑐 ( 𝑘 · 𝐴 ) ) = ( 𝑃 ↑𝑐 ( 𝐴 · 𝑘 ) ) )
29	4	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑃 ∈ ℕ )
30	29	nnrpd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑃 ∈ ℝ+ )
31	24	nn0red	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
32	30 31 26	cxpmuld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ↑𝑐 ( 𝑘 · 𝐴 ) ) = ( ( 𝑃 ↑𝑐 𝑘 ) ↑𝑐 𝐴 ) )
33	29	nncnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑃 ∈ ℂ )
34		cxpexp	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 ↑𝑐 𝑘 ) = ( 𝑃 ↑ 𝑘 ) )
35	33 24 34	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ↑𝑐 𝑘 ) = ( 𝑃 ↑ 𝑘 ) )
36	35	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑃 ↑𝑐 𝑘 ) ↑𝑐 𝐴 ) = ( ( 𝑃 ↑ 𝑘 ) ↑𝑐 𝐴 ) )
37	32 36	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ↑𝑐 ( 𝑘 · 𝐴 ) ) = ( ( 𝑃 ↑ 𝑘 ) ↑𝑐 𝐴 ) )
38	33 26 24	cxpmul2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ↑𝑐 ( 𝐴 · 𝑘 ) ) = ( ( 𝑃 ↑𝑐 𝐴 ) ↑ 𝑘 ) )
39	28 37 38	3eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑃 ↑ 𝑘 ) ↑𝑐 𝐴 ) = ( ( 𝑃 ↑𝑐 𝐴 ) ↑ 𝑘 ) )
40	39	sumeq2dv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑃 ↑ 𝑘 ) ↑𝑐 𝐴 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑃 ↑𝑐 𝐴 ) ↑ 𝑘 ) )
41	8 22 40	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 σ ( 𝑃 ↑ 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑃 ↑𝑐 𝐴 ) ↑ 𝑘 ) )