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 =\left(x\in ℂ,n\in \mathbb{N}⟼\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgm	$$class\sigma$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vn	$$setvarn$$
4		cn	$$class\mathbb{N}$$
5		vk	$$setvark$$
6		vp	$$setvarp$$
7	6	cv	$$setvarp$$
8		cdvds	$$class\parallel$$
9	3	cv	$$setvarn$$
10	7 9 8	wbr	$$wffp\parallel n$$
11	10 6 4	crab	$$class\left\{p\in \mathbb{N}|p\parallel n\right\}$$
12	5	cv	$$setvark$$
13		ccxp	$$class{\uparrow }_c$$
14	1	cv	$$setvarx$$
15	12 14 13	co	$$class{k}^x$$
16	11 15 5	csu	$$class\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x$$
17	1 3 2 4 16	cmpo	$$class\left(x\in ℂ,n\in \mathbb{N}⟼\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\right)$$
18	0 17	wceq	$$wff\sigma =\left(x\in ℂ,n\in \mathbb{N}⟼\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\right)$$