![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-sgm | Structured version Visualization version GIF version |
Description: Define the sum of positive divisors function (𝑥 σ 𝑛), which is the sum of the xth powers of the positive integer divisors of n, see definition in [ApostolNT] p. 38. For 𝑥 = 0, (𝑥 σ 𝑛) counts the number of divisors of 𝑛, i.e. (0 σ 𝑛) is the divisor function, see remark in [ApostolNT] p. 38. (Contributed by Mario Carneiro, 22-Sep-2014.) |
Ref | Expression |
---|---|
df-sgm | ⊢ σ = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛} (𝑘↑𝑐𝑥)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csgm 24622 | . 2 class σ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vn | . . 3 setvar 𝑛 | |
4 | cc 9813 | . . 3 class ℂ | |
5 | cn 10897 | . . 3 class ℕ | |
6 | vp | . . . . . . 7 setvar 𝑝 | |
7 | 6 | cv 1474 | . . . . . 6 class 𝑝 |
8 | 3 | cv 1474 | . . . . . 6 class 𝑛 |
9 | cdvds 14821 | . . . . . 6 class ∥ | |
10 | 7, 8, 9 | wbr 4583 | . . . . 5 wff 𝑝 ∥ 𝑛 |
11 | 10, 6, 5 | crab 2900 | . . . 4 class {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛} |
12 | vk | . . . . . 6 setvar 𝑘 | |
13 | 12 | cv 1474 | . . . . 5 class 𝑘 |
14 | 2 | cv 1474 | . . . . 5 class 𝑥 |
15 | ccxp 24106 | . . . . 5 class ↑𝑐 | |
16 | 13, 14, 15 | co 6549 | . . . 4 class (𝑘↑𝑐𝑥) |
17 | 11, 16, 12 | csu 14264 | . . 3 class Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛} (𝑘↑𝑐𝑥) |
18 | 2, 3, 4, 5, 17 | cmpt2 6551 | . 2 class (𝑥 ∈ ℂ, 𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛} (𝑘↑𝑐𝑥)) |
19 | 1, 18 | wceq 1475 | 1 wff σ = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛} (𝑘↑𝑐𝑥)) |
Colors of variables: wff setvar class |
This definition is referenced by: sgmval 24668 sgmf 24671 |
Copyright terms: Public domain | W3C validator |