This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑠 ∈ ℕ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 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) )