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

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 ( 𝐴 ∈ ℕ → ( 0 σ 𝐴 ) = ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 sgmval2 ⊢ ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( 0 σ 𝐴 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ( 𝑘 ↑ 0 ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℕ → ( 0 σ 𝐴 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ( 𝑘 ↑ 0 ) )
4 elrabi ⊢ ( 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } → 𝑘 ∈ ℕ )
5 4 nncnd ⊢ ( 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } → 𝑘 ∈ ℂ )
6 5 exp0d ⊢ ( 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } → ( 𝑘 ↑ 0 ) = 1 )
7 6 sumeq2i ⊢ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ( 𝑘 ↑ 0 ) = Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } 1
8 dvdsfi ⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
9 ax-1cn ⊢ 1 ∈ ℂ
10 fsumconst ⊢ ( ( { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } 1 = ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) )
11 8 9 10 sylancl ⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } 1 = ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) )
12 7 11 eqtrid ⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ( 𝑘 ↑ 0 ) = ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) )
13 hashcl ⊢ ( { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ∈ Fin → ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
14 8 13 syl ⊢ ( 𝐴 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
15 14 nn0cnd ⊢ ( 𝐴 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℂ )
16 15 mulridd ⊢ ( 𝐴 ∈ ℕ → ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) = ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) )
17 3 12 16 3eqtrd ⊢ ( 𝐴 ∈ ℕ → ( 0 σ 𝐴 ) = ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) )