| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpr |
|- ( ( x = A /\ n = B ) -> n = B ) |
| 2 |
1
|
breq2d |
|- ( ( x = A /\ n = B ) -> ( p || n <-> p || B ) ) |
| 3 |
2
|
rabbidv |
|- ( ( x = A /\ n = B ) -> { p e. NN | p || n } = { p e. NN | p || B } ) |
| 4 |
|
simpll |
|- ( ( ( x = A /\ n = B ) /\ k e. { p e. NN | p || n } ) -> x = A ) |
| 5 |
4
|
oveq2d |
|- ( ( ( x = A /\ n = B ) /\ k e. { p e. NN | p || n } ) -> ( k ^c x ) = ( k ^c A ) ) |
| 6 |
3 5
|
sumeq12dv |
|- ( ( x = A /\ n = B ) -> sum_ k e. { p e. NN | p || n } ( k ^c x ) = sum_ k e. { p e. NN | p || B } ( k ^c A ) ) |
| 7 |
|
df-sgm |
|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) ) |
| 8 |
|
sumex |
|- sum_ k e. { p e. NN | p || B } ( k ^c A ) e. _V |
| 9 |
6 7 8
|
ovmpoa |
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^c A ) ) |