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 = ( 𝑠 ∈ ℕ0 ↦ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crepr	⊢ repr
1		vs	⊢ 𝑠
2		cn0	⊢ ℕ0
3		vb	⊢ 𝑏
4		cn	⊢ ℕ
5	4	cpw	⊢ 𝒫 ℕ
6		vm	⊢ 𝑚
7		cz	⊢ ℤ
8		vc	⊢ 𝑐
9	3	cv	⊢ 𝑏
10		cmap	⊢ ↑m
11		cc0	⊢ 0
12		cfzo	⊢ ..^
13	1	cv	⊢ 𝑠
14	11 13 12	co	⊢ ( 0 ..^ 𝑠 )
15	9 14 10	co	⊢ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) )
16		va	⊢ 𝑎
17	8	cv	⊢ 𝑐
18	16	cv	⊢ 𝑎
19	18 17	cfv	⊢ ( 𝑐 ‘ 𝑎 )
20	14 19 16	csu	⊢ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 )
21	6	cv	⊢ 𝑚
22	20 21	wceq	⊢ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚
23	22 8 15	crab	⊢ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 }
24	3 6 5 7 23	cmpo	⊢ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } )
25	1 2 24	cmpt	⊢ ( 𝑠 ∈ ℕ0 ↦ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) )
26	0 25	wceq	⊢ repr = ( 𝑠 ∈ ℕ0 ↦ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) )