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 ⊢ A ∈ ℂ ∧ B ∈ ℕ → A σ B = ∑ k ∈ p ∈ ℕ | p ∥ B k A

Proof

Step Hyp Ref Expression
1 simpr ⊢ x = A ∧ n = B → n = B
2 1 breq2d ⊢ x = A ∧ n = B → p ∥ n ↔ p ∥ B
3 2 rabbidv ⊢ x = A ∧ n = B → p ∈ ℕ | p ∥ n = p ∈ ℕ | p ∥ B
4 simpll ⊢ x = A ∧ n = B ∧ k ∈ p ∈ ℕ | p ∥ n → x = A
5 4 oveq2d ⊢ x = A ∧ n = B ∧ k ∈ p ∈ ℕ | p ∥ n → k x = k A
6 3 5 sumeq12dv ⊢ x = A ∧ n = B → ∑ k ∈ p ∈ ℕ | p ∥ n k x = ∑ k ∈ p ∈ ℕ | p ∥ B k A
7 df-sgm ⊢ σ = x ∈ ℂ , n ∈ ℕ ⟼ ∑ k ∈ p ∈ ℕ | p ∥ n k x
8 sumex ⊢ ∑ k ∈ p ∈ ℕ | p ∥ B k A ∈ V
9 6 7 8 ovmpoa ⊢ A ∈ ℂ ∧ B ∈ ℕ → A σ B = ∑ k ∈ p ∈ ℕ | p ∥ B k A