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		dvdsfi	|- ( A e. NN -> { p e. NN | p || A } e. Fin )
9		ax-1cn	|- 1 e. CC
10		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 ) )
11	8 9 10	sylancl	|- ( A e. NN -> sum_ k e. { p e. NN | p || A } 1 = ( ( # ` { p e. NN | p || A } ) x. 1 ) )
12	7 11	eqtrid	|- ( A e. NN -> sum_ k e. { p e. NN | p || A } ( k ^ 0 ) = ( ( # ` { p e. NN | p || A } ) x. 1 ) )
13		hashcl	|- ( { p e. NN | p || A } e. Fin -> ( # ` { p e. NN | p || A } ) e. NN0 )
14	8 13	syl	|- ( A e. NN -> ( # ` { p e. NN | p || A } ) e. NN0 )
15	14	nn0cnd	|- ( A e. NN -> ( # ` { p e. NN | p || A } ) e. CC )
16	15	mulridd	|- ( A e. NN -> ( ( # ` { p e. NN | p || A } ) x. 1 ) = ( # ` { p e. NN | p || A } ) )
17	3 12 16	3eqtrd	|- ( A e. NN -> ( 0 sigma A ) = ( # ` { p e. NN | p || A } ) )