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