Theorem sgmval

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

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

Proof

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