Metamath Proof Explorer

Theorem sgmval2

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

Ref Expression
Assertion sgmval2 ⊢ A ∈ ℤ ∧ B ∈ ℕ → A σ B = ∑ k ∈ p ∈ ℕ | p ∥ B k A

Proof

Step Hyp Ref Expression
1 zcn ⊢ A ∈ ℤ → A ∈ ℂ
2 sgmval ⊢ A ∈ ℂ ∧ B ∈ ℕ → A σ B = ∑ k ∈ p ∈ ℕ | p ∥ B k A
3 1 2 sylan ⊢ A ∈ ℤ ∧ B ∈ ℕ → A σ B = ∑ k ∈ p ∈ ℕ | p ∥ B k A
4 ssrab2 ⊢ p ∈ ℕ | p ∥ B ⊆ ℕ
5 simpr ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ k ∈ p ∈ ℕ | p ∥ B → k ∈ p ∈ ℕ | p ∥ B
6 4 5 sseldi ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ k ∈ p ∈ ℕ | p ∥ B → k ∈ ℕ
7 6 nncnd ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ k ∈ p ∈ ℕ | p ∥ B → k ∈ ℂ
8 6 nnne0d ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ k ∈ p ∈ ℕ | p ∥ B → k ≠ 0
9 simpll ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ k ∈ p ∈ ℕ | p ∥ B → A ∈ ℤ
10 7 8 9 cxpexpzd ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ k ∈ p ∈ ℕ | p ∥ B → k A = k A
11 10 sumeq2dv ⊢ A ∈ ℤ ∧ B ∈ ℕ → ∑ k ∈ p ∈ ℕ | p ∥ B k A = ∑ k ∈ p ∈ ℕ | p ∥ B k A
12 3 11 eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℕ → A σ B = ∑ k ∈ p ∈ ℕ | p ∥ B k A