Definition df-sgm 15641

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 15640	. 2 class sigma
2		vx	. . 3 setvar x
3		vn	. . 3 setvar n
4		cc 7985	. . 3 class CC
5		cn 9098	. . 3 class NN
6		vp	. . . . . . 7 setvar p
7	6	cv 1394	. . . . . 6 class p
8	3	cv 1394	. . . . . 6 class n
9		cdvds 12284	. . . . . 6 class ||
10	7, 8, 9	wbr 4082	. . . . 5 wff p || n
11	10, 6, 5	crab 2512	. . . 4 class { p e. NN | p || n }
12		vk	. . . . . 6 setvar k
13	12	cv 1394	. . . . 5 class k
14	2	cv 1394	. . . . 5 class x
15		ccxp 15516	. . . . 5 class ^c
16	13, 14, 15	co 5994	. . . 4 class ( k ^c x )
17	11, 16, 12	csu 11850	. . 3 class sum_ k e. { p e. NN | p || n } ( k ^c x )
18	2, 3, 4, 5, 17	cmpo 5996	. 2 class ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
19	1, 18	wceq 1395	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  15642  sgmf  15645