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		fzfid	⊢ ( 𝐴 ∈ ℕ → ( 1 ... 𝐴 ) ∈ Fin )
9		dvdsssfz1	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )
10	8 9	ssfid	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
11		ax-1cn	⊢ 1 ∈ ℂ
12		fsumconst	⊢ ( ( { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } 1 = ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) )
13	10 11 12	sylancl	⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } 1 = ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) )
14	7 13	syl5eq	⊢ ( 𝐴 ∈ ℕ → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ( 𝑘 ↑ 0 ) = ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) )
15		hashcl	⊢ ( { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ∈ Fin → ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
16	10 15	syl	⊢ ( 𝐴 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
17	16	nn0cnd	⊢ ( 𝐴 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℂ )
18	17	mulid1d	⊢ ( 𝐴 ∈ ℕ → ( ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) · 1 ) = ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) )
19	3 14 18	3eqtrd	⊢ ( 𝐴 ∈ ℕ → ( 0 σ 𝐴 ) = ( ♯ ‘ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ) )