Theorem 0sgm

Description: The value of the sum-of-divisors function, usually denoted σ₀(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 σ 𝐴 ) = ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) )