This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )