Metamath Proof Explorer

Theorem 0sgm

Description: The value of the sum-of-divisors function, usually denoted σ0(n). (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion 0sgm ⊢ A ∈ ℕ → 0 σ A = p ∈ ℕ | p ∥ A

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 sgmval2 ⊢ 0 ∈ ℤ ∧ A ∈ ℕ → 0 σ A = ∑ k ∈ p ∈ ℕ | p ∥ A k 0
3 1 2 mpan ⊢ A ∈ ℕ → 0 σ A = ∑ k ∈ p ∈ ℕ | p ∥ A k 0
4 elrabi ⊢ k ∈ p ∈ ℕ | p ∥ A → k ∈ ℕ
5 4 nncnd ⊢ k ∈ p ∈ ℕ | p ∥ A → k ∈ ℂ
6 5 exp0d ⊢ k ∈ p ∈ ℕ | p ∥ A → k 0 = 1
7 6 sumeq2i ⊢ ∑ k ∈ p ∈ ℕ | p ∥ A k 0 = ∑ k ∈ p ∈ ℕ | p ∥ A 1
8 dvdsfi ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ∈ Fin
9 ax-1cn ⊢ 1 ∈ ℂ
10 fsumconst ⊢ p ∈ ℕ | p ∥ A ∈ Fin ∧ 1 ∈ ℂ → ∑ k ∈ p ∈ ℕ | p ∥ A 1 = p ∈ ℕ | p ∥ A ⋅ 1
11 8 9 10 sylancl ⊢ A ∈ ℕ → ∑ k ∈ p ∈ ℕ | p ∥ A 1 = p ∈ ℕ | p ∥ A ⋅ 1
12 7 11 eqtrid ⊢ A ∈ ℕ → ∑ k ∈ p ∈ ℕ | p ∥ A k 0 = p ∈ ℕ | p ∥ A ⋅ 1
13 hashcl ⊢ p ∈ ℕ | p ∥ A ∈ Fin → p ∈ ℕ | p ∥ A ∈ ℕ 0
14 8 13 syl ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ∈ ℕ 0
15 14 nn0cnd ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ∈ ℂ
16 15 mulridd ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ⋅ 1 = p ∈ ℕ | p ∥ A
17 3 12 16 3eqtrd ⊢ A ∈ ℕ → 0 σ A = p ∈ ℕ | p ∥ A