This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ... 𝑁 ) ( ( 𝑃 ↑𝑐 𝐴 ) ↑ 𝑘 ) )