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

Metamath Proof Explorer

Definition df-sgm

Detailed syntax breakdown