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	|- ( A e. NN -> ( 0 sigma A ) = ( # ` { p e. NN | p || A } ) )

Proof

Step	Hyp	Ref	Expression
1		0z	|- 0 e. ZZ
2		sgmval2	|- ( ( 0 e. ZZ /\ A e. NN ) -> ( 0 sigma A ) = sum_ k e. { p e. NN | p || A } ( k ^ 0 ) )
3	1 2	mpan	|- ( A e. NN -> ( 0 sigma A ) = sum_ k e. { p e. NN | p || A } ( k ^ 0 ) )
4		elrabi	|- ( k e. { p e. NN | p || A } -> k e. NN )
5	4	nncnd	|- ( k e. { p e. NN | p || A } -> k e. CC )
6	5	exp0d	|- ( k e. { p e. NN | p || A } -> ( k ^ 0 ) = 1 )
7	6	sumeq2i	|- sum_ k e. { p e. NN | p || A } ( k ^ 0 ) = sum_ k e. { p e. NN | p || A } 1
8		fzfid	|- ( A e. NN -> ( 1 ... A ) e. Fin )
9		dvdsssfz1	|- ( A e. NN -> { p e. NN | p || A } C_ ( 1 ... A ) )
10	8 9	ssfid	|- ( A e. NN -> { p e. NN | p || A } e. Fin )
11		ax-1cn	|- 1 e. CC
12		fsumconst	|- ( ( { p e. NN | p || A } e. Fin /\ 1 e. CC ) -> sum_ k e. { p e. NN | p || A } 1 = ( ( # ` { p e. NN | p || A } ) x. 1 ) )
13	10 11 12	sylancl	|- ( A e. NN -> sum_ k e. { p e. NN | p || A } 1 = ( ( # ` { p e. NN | p || A } ) x. 1 ) )
14	7 13	syl5eq	|- ( A e. NN -> sum_ k e. { p e. NN | p || A } ( k ^ 0 ) = ( ( # ` { p e. NN | p || A } ) x. 1 ) )
15		hashcl	|- ( { p e. NN | p || A } e. Fin -> ( # ` { p e. NN | p || A } ) e. NN0 )
16	10 15	syl	|- ( A e. NN -> ( # ` { p e. NN | p || A } ) e. NN0 )
17	16	nn0cnd	|- ( A e. NN -> ( # ` { p e. NN | p || A } ) e. CC )
18	17	mulid1d	|- ( A e. NN -> ( ( # ` { p e. NN | p || A } ) x. 1 ) = ( # ` { p e. NN | p || A } ) )
19	3 14 18	3eqtrd	|- ( A e. NN -> ( 0 sigma A ) = ( # ` { p e. NN | p || A } ) )