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

Definition df-sgm 20339
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 20333 . 2  class  sigma
2 vx . . 3  set  x
3 vn . . 3  set  n
4 cc 8735 . . 3  class  CC
5 cn 9746 . . 3  class  NN
6 vp . . . . . . 7  set  p
76cv 1622 . . . . . 6  class  p
83cv 1622 . . . . . 6  class  n
9 cdivides 12531 . . . . . 6  class  ||
107, 8, 9wbr 4023 . . . . 5  wff  p  ||  n
1110, 6, 5crab 2547 . . . 4  class  { p  e.  NN  |  p  ||  n }
12 vk . . . . . 6  set  k
1312cv 1622 . . . . 5  class  k
142cv 1622 . . . . 5  class  x
15 ccxp 19913 . . . . 5  class  ^ c
1613, 14, 15co 5858 . . . 4  class  ( k  ^ c  x )
1711, 16, 12csu 12158 . . 3  class  sum_ k  e.  { p  e.  NN  |  p  ||  n } 
( k  ^ c  x )
182, 3, 4, 5, 17cmpt2 5860 . 2  class  ( x  e.  CC ,  n  e.  NN  |->  sum_ k  e.  {
p  e.  NN  |  p  ||  n }  (
k  ^ c  x ) )
191, 18wceq 1623 1  wff  sigma  =  ( x  e.  CC ,  n  e.  NN  |->  sum_ k  e.  { p  e.  NN  |  p  ||  n } 
( k  ^ c  x ) )
Colors of variables: wff set class
This definition is referenced by:  sgmval  20380  sgmf  20383
  Copyright terms: Public domain W3C validator