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 σ = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝𝑛 } ( 𝑘𝑐 𝑥 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csgm σ
1 vx 𝑥
2 cc
3 vn 𝑛
4 cn
5 vk 𝑘
6 vp 𝑝
7 6 cv 𝑝
8 cdvds
9 3 cv 𝑛
10 7 9 8 wbr 𝑝𝑛
11 10 6 4 crab { 𝑝 ∈ ℕ ∣ 𝑝𝑛 }
12 5 cv 𝑘
13 ccxp 𝑐
14 1 cv 𝑥
15 12 14 13 co ( 𝑘𝑐 𝑥 )
16 11 15 5 csu Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝𝑛 } ( 𝑘𝑐 𝑥 )
17 1 3 2 4 16 cmpo ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝𝑛 } ( 𝑘𝑐 𝑥 ) )
18 0 17 wceq σ = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝𝑛 } ( 𝑘𝑐 𝑥 ) )