MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sgm Structured version   Unicode version

Definition df-sgm 22571
Description: Define the divisor function, which counts the number of divisors of  n, to the power  x. (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
StepHypRef Expression
1 csgm 22565 . 2  class  sigma
2 vx . . 3  setvar  x
3 vn . . 3  setvar  n
4 cc 9390 . . 3  class  CC
5 cn 10432 . . 3  class  NN
6 vp . . . . . . 7  setvar  p
76cv 1369 . . . . . 6  class  p
83cv 1369 . . . . . 6  class  n
9 cdivides 13652 . . . . . 6  class  ||
107, 8, 9wbr 4399 . . . . 5  wff  p  ||  n
1110, 6, 5crab 2802 . . . 4  class  { p  e.  NN  |  p  ||  n }
12 vk . . . . . 6  setvar  k
1312cv 1369 . . . . 5  class  k
142cv 1369 . . . . 5  class  x
15 ccxp 22139 . . . . 5  class  ^c
1613, 14, 15co 6199 . . . 4  class  ( k  ^c  x )
1711, 16, 12csu 13280 . . 3  class  sum_ k  e.  { p  e.  NN  |  p  ||  n } 
( k  ^c 
x )
182, 3, 4, 5, 17cmpt2 6201 . 2  class  ( x  e.  CC ,  n  e.  NN  |->  sum_ k  e.  {
p  e.  NN  |  p  ||  n }  (
k  ^c  x ) )
191, 18wceq 1370 1  wff  sigma  =  ( x  e.  CC ,  n  e.  NN  |->  sum_ k  e.  { p  e.  NN  |  p  ||  n } 
( k  ^c 
x ) )
Colors of variables: wff setvar class
This definition is referenced by:  sgmval  22612  sgmf  22615
  Copyright terms: Public domain W3C validator