Definition df-repr 30687

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

Assertion

Ref	Expression
df-repr	|- repr = ( s e. NN0 |-> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0..^ s ) ) | sum_ a e. ( 0..^ s ) ( c ` a ) = m } ) )

Distinct variable group:   a, b, c, m, s

Detailed syntax breakdown of Definition df-repr

Step	Hyp	Ref	Expression
1		crepr 30686	. 2 class repr
2		vs	. . 3 setvar s
3		cn0 11292	. . 3 class NN0
4		vb	. . . 4 setvar b
5		vm	. . . 4 setvar m
6		cn 11020	. . . . 5 class NN
7	6	cpw 4158	. . . 4 class ~P NN
8		cz 11377	. . . 4 class ZZ
9		cc0 9936	. . . . . . . 8 class 0
10	2	cv 1482	. . . . . . . 8 class s
11		cfzo 12465	. . . . . . . 8 class ..^
12	9, 10, 11	co 6650	. . . . . . 7 class ( 0..^ s )
13		va	. . . . . . . . 9 setvar a
14	13	cv 1482	. . . . . . . 8 class a
15		vc	. . . . . . . . 9 setvar c
16	15	cv 1482	. . . . . . . 8 class c
17	14, 16	cfv 5888	. . . . . . 7 class ( c ` a )
18	12, 17, 13	csu 14416	. . . . . 6 class sum_ a e. ( 0..^ s ) ( c ` a )
19	5	cv 1482	. . . . . 6 class m
20	18, 19	wceq 1483	. . . . 5 wff sum_ a e. ( 0..^ s ) ( c ` a ) = m
21	4	cv 1482	. . . . . 6 class b
22		cmap 7857	. . . . . 6 class ^m
23	21, 12, 22	co 6650	. . . . 5 class ( b ^m ( 0..^ s ) )
24	20, 15, 23	crab 2916	. . . 4 class { c e. ( b ^m ( 0..^ s ) ) | sum_ a e. ( 0..^ s ) ( c ` a ) = m }
25	4, 5, 7, 8, 24	cmpt2 6652	. . 3 class ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0..^ s ) ) | sum_ a e. ( 0..^ s ) ( c ` a ) = m } )
26	2, 3, 25	cmpt 4729	. 2 class ( s e. NN0 |-> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0..^ s ) ) | sum_ a e. ( 0..^ s ) ( c ` a ) = m } ) )
27	1, 26	wceq 1483	1 wff repr = ( s e. NN0 |-> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0..^ s ) ) | sum_ a e. ( 0..^ s ) ( c ` a ) = m } ) )

This definition is referenced by:  reprval  30688