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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ( 𝑘 ↑𝑐 𝐴 ) )