Definition df-sgm

Description: Define the sum of positive divisors function ( x sigma n ) , which is the sum of the xth powers of the positive integer divisors of n, see definition in ApostolNT p. 38. For x = 0 , ( x sigma n ) counts the number of divisors of n , i.e. ( 0 sigma n ) isthe divisor function, see remark in ApostolNT p. 38. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	df-sgm	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgm	|- sigma
1		vx	|- x
2		cc	|- CC
3		vn	|- n
4		cn	|- NN
5		vk	|- k
6		vp	|- p
7	6	cv	|- p
8		cdvds	|- ||
9	3	cv	|- n
10	7 9 8	wbr	|- p || n
11	10 6 4	crab	|- { p e. NN | p || n }
12	5	cv	|- k
13		ccxp	|- ^c
14	1	cv	|- x
15	12 14 13	co	|- ( k ^c x )
16	11 15 5	csu	|- sum_ k e. { p e. NN | p || n } ( k ^c x )
17	1 3 2 4 16	cmpo	|- ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
18	0 17	wceq	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )