Theorem sgmval

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

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

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑛 = 𝐵 ) → 𝑛 = 𝐵 )
2	1	breq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑛 = 𝐵 ) → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝐵 ) )
3	2	rabbidv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑛 = 𝐵 ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } = { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } )
4		simpll	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑛 = 𝐵 ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ) → 𝑥 = 𝐴 )
5	4	oveq2d	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑛 = 𝐵 ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ) → ( 𝑘 ↑𝑐 𝑥 ) = ( 𝑘 ↑𝑐 𝐴 ) )
6	3 5	sumeq12dv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑛 = 𝐵 ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ( 𝑘 ↑𝑐 𝑥 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) )
7		df-sgm	⊢ σ = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ( 𝑘 ↑𝑐 𝑥 ) )
8		sumex	⊢ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) ∈ V
9	6 7 8	ovmpoa	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) )