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 
|- ( 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 } ) )