Metamath Proof Explorer

Definition df-repr

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)

Ref Expression
Assertion 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 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crepr 
 |-  repr
1 vs 
 |-  s
2 cn0 
 |-  NN0
3 vb 
 |-  b
4 cn 
 |-  NN
5 4 cpw 
 |-  ~P NN
6 vm 
 |-  m
7 cz 
 |-  ZZ
8 vc 
 |-  c
9 3 cv 
 |-  b
10 cmap 
 |-  ^m
11 cc0 
 |-  0
12 cfzo 
 |-  ..^
13 1 cv 
 |-  s
14 11 13 12 co 
 |-  ( 0 ..^ s )
15 9 14 10 co 
 |-  ( b ^m ( 0 ..^ s ) )
16 va 
 |-  a
17 8 cv 
 |-  c
18 16 cv 
 |-  a
19 18 17 cfv 
 |-  ( c ` a )
20 14 19 16 csu 
 |-  sum_ a e. ( 0 ..^ s ) ( c ` a )
21 6 cv 
 |-  m
22 20 21 wceq 
 |-  sum_ a e. ( 0 ..^ s ) ( c ` a ) = m
23 22 8 15 crab 
 |-  { c e. ( b ^m ( 0 ..^ s ) ) | sum_ a e. ( 0 ..^ s ) ( c ` a ) = m }
24 3 6 5 7 23 cmpo 
 |-  ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ s ) ) | sum_ a e. ( 0 ..^ s ) ( c ` a ) = m } )
25 1 2 24 cmpt 
 |-  ( s e. NN0 |-> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ s ) ) | sum_ a e. ( 0 ..^ s ) ( c ` a ) = m } ) )
26 0 25 wceq 
 |-  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 } ) )