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