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 = s ∈ ℕ 0 ⟼ b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m

Detailed syntax breakdown

Step Hyp Ref Expression
0 crepr class repr
1 vs setvar s
2 cn0 class ℕ 0
3 vb setvar b
4 cn class ℕ
5 4 cpw class 𝒫 ℕ
6 vm setvar m
7 cz class ℤ
8 vc setvar c
9 3 cv setvar b
10 cmap class ↑ 𝑚
11 cc0 class 0
12 cfzo class ..^
13 1 cv setvar s
14 11 13 12 co class 0 ..^ s
15 9 14 10 co class b 0 ..^ s
16 va setvar a
17 8 cv setvar c
18 16 cv setvar a
19 18 17 cfv class c ⁡ a
20 14 19 16 csu class ∑ a ∈ 0 ..^ s c ⁡ a
21 6 cv setvar m
22 20 21 wceq wff ∑ a ∈ 0 ..^ s c ⁡ a = m
23 22 8 15 crab class c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m
24 3 6 5 7 23 cmpo class b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m
25 1 2 24 cmpt class s ∈ ℕ 0 ⟼ b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m
26 0 25 wceq wff repr = s ∈ ℕ 0 ⟼ b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m