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 fzfid ⊢ A ∈ ℕ → 1 … A ∈ Fin
9 dvdsssfz1 ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ⊆ 1 … A
10 8 9 ssfid ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ∈ Fin
11 ax-1cn ⊢ 1 ∈ ℂ
12 fsumconst ⊢ p ∈ ℕ | p ∥ A ∈ Fin ∧ 1 ∈ ℂ → ∑ k ∈ p ∈ ℕ | p ∥ A 1 = p ∈ ℕ | p ∥ A ⋅ 1
13 10 11 12 sylancl ⊢ A ∈ ℕ → ∑ k ∈ p ∈ ℕ | p ∥ A 1 = p ∈ ℕ | p ∥ A ⋅ 1
14 7 13 syl5eq ⊢ A ∈ ℕ → ∑ k ∈ p ∈ ℕ | p ∥ A k 0 = p ∈ ℕ | p ∥ A ⋅ 1
15 hashcl ⊢ p ∈ ℕ | p ∥ A ∈ Fin → p ∈ ℕ | p ∥ A ∈ ℕ 0
16 10 15 syl ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ∈ ℕ 0
17 16 nn0cnd ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ∈ ℂ
18 17 mulid1d ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ⋅ 1 = p ∈ ℕ | p ∥ A
19 3 14 18 3eqtrd ⊢ A ∈ ℕ → 0 σ A = p ∈ ℕ | p ∥ A