Metamath Proof Explorer

Theorem reprval

Description: Value of the representations of M as the sum of S nonnegative integers in a given set A . (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
Assertion reprval ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ φ → A ⊆ ℕ
2 reprval.m ⊢ φ → M ∈ ℤ
3 reprval.s ⊢ φ → S ∈ ℕ 0
4 df-repr ⊢ repr = s ∈ ℕ 0 ⟼ b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m
5 oveq2 ⊢ s = S → 0 ..^ s = 0 ..^ S
6 5 oveq2d ⊢ s = S → b 0 ..^ s = b 0 ..^ S
7 5 sumeq1d ⊢ s = S → ∑ a ∈ 0 ..^ s c ⁡ a = ∑ a ∈ 0 ..^ S c ⁡ a
8 7 eqeq1d ⊢ s = S → ∑ a ∈ 0 ..^ s c ⁡ a = m ↔ ∑ a ∈ 0 ..^ S c ⁡ a = m
9 6 8 rabeqbidv ⊢ s = S → c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m = c ∈ b 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = m
10 9 mpoeq3dv ⊢ s = S → b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ s | ∑ a ∈ 0 ..^ s c ⁡ a = m = b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = m
11 nnex ⊢ ℕ ∈ V
12 11 pwex ⊢ 𝒫 ℕ ∈ V
13 zex ⊢ ℤ ∈ V
14 12 13 mpoex ⊢ b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = m ∈ V
15 14 a1i ⊢ φ → b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = m ∈ V
16 4 10 3 15 fvmptd3 ⊢ φ → repr ⁡ S = b ∈ 𝒫 ℕ , m ∈ ℤ ⟼ c ∈ b 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = m
17 simprl ⊢ φ ∧ b = A ∧ m = M → b = A
18 17 oveq1d ⊢ φ ∧ b = A ∧ m = M → b 0 ..^ S = A 0 ..^ S
19 simprr ⊢ φ ∧ b = A ∧ m = M → m = M
20 19 eqeq2d ⊢ φ ∧ b = A ∧ m = M → ∑ a ∈ 0 ..^ S c ⁡ a = m ↔ ∑ a ∈ 0 ..^ S c ⁡ a = M
21 18 20 rabeqbidv ⊢ φ ∧ b = A ∧ m = M → c ∈ b 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = m = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
22 11 a1i ⊢ φ → ℕ ∈ V
23 22 1 ssexd ⊢ φ → A ∈ V
24 23 1 elpwd ⊢ φ → A ∈ 𝒫 ℕ
25 ovex ⊢ A 0 ..^ S ∈ V
26 25 rabex ⊢ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ∈ V
27 26 a1i ⊢ φ → c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ∈ V
28 16 21 24 2 27 ovmpod ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M