Metamath Proof Explorer


Theorem sgmval2

Description: The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion sgmval2
|- ( ( A e. ZZ /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )

Proof

Step Hyp Ref Expression
1 zcn
 |-  ( A e. ZZ -> A e. CC )
2 sgmval
 |-  ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^c A ) )
3 1 2 sylan
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^c A ) )
4 ssrab2
 |-  { p e. NN | p || B } C_ NN
5 simpr
 |-  ( ( ( A e. ZZ /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> k e. { p e. NN | p || B } )
6 4 5 sselid
 |-  ( ( ( A e. ZZ /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> k e. NN )
7 6 nncnd
 |-  ( ( ( A e. ZZ /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> k e. CC )
8 6 nnne0d
 |-  ( ( ( A e. ZZ /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> k =/= 0 )
9 simpll
 |-  ( ( ( A e. ZZ /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> A e. ZZ )
10 7 8 9 cxpexpzd
 |-  ( ( ( A e. ZZ /\ B e. NN ) /\ k e. { p e. NN | p || B } ) -> ( k ^c A ) = ( k ^ A ) )
11 10 sumeq2dv
 |-  ( ( A e. ZZ /\ B e. NN ) -> sum_ k e. { p e. NN | p || B } ( k ^c A ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )
12 3 11 eqtrd
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )