Definition df-repr 34624

Description: The representations of a nonnegative 𝑚 as the sum of 𝑠 nonnegative integers from a set 𝑏. Cf. Definition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 1-Dec-2021.)

Assertion

Ref	Expression
df-repr	⊢ repr = (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}))

Distinct variable group:   𝑎,𝑏,𝑐,𝑚,𝑠

Detailed syntax breakdown of Definition df-repr

Step	Hyp	Ref	Expression
1		crepr 34623	. 2 class repr
2		vs	. . 3 setvar 𝑠
3		cn0 12526	. . 3 class ℕ0
4		vb	. . . 4 setvar 𝑏
5		vm	. . . 4 setvar 𝑚
6		cn 12266	. . . . 5 class ℕ
7	6	cpw 4600	. . . 4 class 𝒫 ℕ
8		cz 12613	. . . 4 class ℤ
9		cc0 11155	. . . . . . . 8 class 0
10	2	cv 1539	. . . . . . . 8 class 𝑠
11		cfzo 13694	. . . . . . . 8 class ..^
12	9, 10, 11	co 7431	. . . . . . 7 class (0..^𝑠)
13		va	. . . . . . . . 9 setvar 𝑎
14	13	cv 1539	. . . . . . . 8 class 𝑎
15		vc	. . . . . . . . 9 setvar 𝑐
16	15	cv 1539	. . . . . . . 8 class 𝑐
17	14, 16	cfv 6561	. . . . . . 7 class (𝑐‘𝑎)
18	12, 17, 13	csu 15722	. . . . . 6 class Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎)
19	5	cv 1539	. . . . . 6 class 𝑚
20	18, 19	wceq 1540	. . . . 5 wff Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚
21	4	cv 1539	. . . . . 6 class 𝑏
22		cmap 8866	. . . . . 6 class ↑m
23	21, 12, 22	co 7431	. . . . 5 class (𝑏 ↑m (0..^𝑠))
24	20, 15, 23	crab 3436	. . . 4 class {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}
25	4, 5, 7, 8, 24	cmpo 7433	. . 3 class (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚})
26	2, 3, 25	cmpt 5225	. 2 class (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}))
27	1, 26	wceq 1540	1 wff repr = (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}))

This definition is referenced by:  reprval  34625