Theorem sgmval2

Description: The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	sgmval2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2		sgmval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) )
4		ssrab2	⊢ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ⊆ ℕ
5		simpr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } )
6	4 5	sseldi	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ∈ ℕ )
7	6	nncnd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ∈ ℂ )
8	6	nnne0d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝑘 ≠ 0 )
9		simpll	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → 𝐴 ∈ ℤ )
10	7 8 9	cxpexpzd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ) → ( 𝑘 ↑𝑐 𝐴 ) = ( 𝑘 ↑ 𝐴 ) )
11	10	sumeq2dv	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )
12	3 11	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑ 𝐴 ) )