Definition df-repr 32489

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 32488	. 2 class repr
2		vs	. . 3 setvar 𝑠
3		cn0 12163	. . 3 class ℕ0
4		vb	. . . 4 setvar 𝑏
5		vm	. . . 4 setvar 𝑚
6		cn 11903	. . . . 5 class ℕ
7	6	cpw 4530	. . . 4 class 𝒫 ℕ
8		cz 12249	. . . 4 class ℤ
9		cc0 10802	. . . . . . . 8 class 0
10	2	cv 1538	. . . . . . . 8 class 𝑠
11		cfzo 13311	. . . . . . . 8 class ..^
12	9, 10, 11	co 7255	. . . . . . 7 class (0..^𝑠)
13		va	. . . . . . . . 9 setvar 𝑎
14	13	cv 1538	. . . . . . . 8 class 𝑎
15		vc	. . . . . . . . 9 setvar 𝑐
16	15	cv 1538	. . . . . . . 8 class 𝑐
17	14, 16	cfv 6418	. . . . . . 7 class (𝑐‘𝑎)
18	12, 17, 13	csu 15325	. . . . . 6 class Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎)
19	5	cv 1538	. . . . . 6 class 𝑚
20	18, 19	wceq 1539	. . . . 5 wff Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚
21	4	cv 1538	. . . . . 6 class 𝑏
22		cmap 8573	. . . . . 6 class ↑m
23	21, 12, 22	co 7255	. . . . 5 class (𝑏 ↑m (0..^𝑠))
24	20, 15, 23	crab 3067	. . . 4 class {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}
25	4, 5, 7, 8, 24	cmpo 7257	. . 3 class (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚})
26	2, 3, 25	cmpt 5153	. 2 class (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}))
27	1, 26	wceq 1539	1 wff repr = (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐‘𝑎) = 𝑚}))

This definition is referenced by:  reprval  32490