Definition df-sgm 15712

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 ) is the divisor function, see remark in [ApostolNT] p. 38. (Contributed by Mario Carneiro, 22-Sep-2014.)

Assertion

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

Distinct variable group:   x, n, k, p

Detailed syntax breakdown of Definition df-sgm

Step	Hyp	Ref	Expression
1		csgm 15711	. 2 class sigma
2		vx	. . 3 setvar x
3		vn	. . 3 setvar n
4		cc 8030	. . 3 class CC
5		cn 9143	. . 3 class NN
6		vp	. . . . . . 7 setvar p
7	6	cv 1396	. . . . . 6 class p
8	3	cv 1396	. . . . . 6 class n
9		cdvds 12353	. . . . . 6 class ||
10	7, 8, 9	wbr 4088	. . . . 5 wff p || n
11	10, 6, 5	crab 2514	. . . 4 class { p e. NN | p || n }
12		vk	. . . . . 6 setvar k
13	12	cv 1396	. . . . 5 class k
14	2	cv 1396	. . . . 5 class x
15		ccxp 15587	. . . . 5 class ^c
16	13, 14, 15	co 6018	. . . 4 class ( k ^c x )
17	11, 16, 12	csu 11918	. . 3 class sum_ k e. { p e. NN | p || n } ( k ^c x )
18	2, 3, 4, 5, 17	cmpo 6020	. 2 class ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
19	1, 18	wceq 1397	1 wff sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )

This definition is referenced by:  sgmval  15713  sgmf  15716