Definition df-sgm 24828

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:   k, n, p, x

Detailed syntax breakdown of Definition df-sgm

Step	Hyp	Ref	Expression
1		csgm 24822	. 2 class sigma
2		vx	. . 3 setvar x
3		vn	. . 3 setvar n
4		cc 9934	. . 3 class CC
5		cn 11020	. . 3 class NN
6		vp	. . . . . . 7 setvar p
7	6	cv 1482	. . . . . 6 class p
8	3	cv 1482	. . . . . 6 class n
9		cdvds 14983	. . . . . 6 class ||
10	7, 8, 9	wbr 4653	. . . . 5 wff p || n
11	10, 6, 5	crab 2916	. . . 4 class { p e. NN | p || n }
12		vk	. . . . . 6 setvar k
13	12	cv 1482	. . . . 5 class k
14	2	cv 1482	. . . . 5 class x
15		ccxp 24302	. . . . 5 class ^c
16	13, 14, 15	co 6650	. . . 4 class ( k ^c x )
17	11, 16, 12	csu 14416	. . 3 class sum_ k e. { p e. NN | p || n } ( k ^c x )
18	2, 3, 4, 5, 17	cmpt2 6652	. 2 class ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
19	1, 18	wceq 1483	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  24868  sgmf  24871