Metamath Proof Explorer

Theorem smupval

Description: Rewrite the elements of the partial sum sequence in terms of sequence multiplication. (Contributed by Mario Carneiro, 20-Sep-2016)

Ref Expression
Hypotheses smupval.a ⊢ φ → A ⊆ ℕ 0
smupval.b ⊢ φ → B ⊆ ℕ 0
smupval.p ⊢ P = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
smupval.n ⊢ φ → N ∈ ℕ 0
Assertion smupval ⊢ φ → P ⁡ N = A ∩ 0 ..^ N smul B

Proof

Step Hyp Ref Expression
1 smupval.a ⊢ φ → A ⊆ ℕ 0
2 smupval.b ⊢ φ → B ⊆ ℕ 0
3 smupval.p ⊢ P = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 smupval.n ⊢ φ → N ∈ ℕ 0
5 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
6 4 5 eleqtrdi ⊢ φ → N ∈ ℤ ≥ 0
7 eluzfz2b ⊢ N ∈ ℤ ≥ 0 ↔ N ∈ 0 … N
8 6 7 sylib ⊢ φ → N ∈ 0 … N
9 fveq2 ⊢ x = 0 → P ⁡ x = P ⁡ 0
10 fveq2 ⊢ x = 0 → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
11 9 10 eqeq12d ⊢ x = 0 → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ P ⁡ 0 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
12 11 imbi2d ⊢ x = 0 → φ → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ φ → P ⁡ 0 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
13 fveq2 ⊢ x = k → P ⁡ x = P ⁡ k
14 fveq2 ⊢ x = k → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
15 13 14 eqeq12d ⊢ x = k → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ P ⁡ k = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
16 15 imbi2d ⊢ x = k → φ → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ φ → P ⁡ k = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k
17 fveq2 ⊢ x = k + 1 → P ⁡ x = P ⁡ k + 1
18 fveq2 ⊢ x = k + 1 → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1
19 17 18 eqeq12d ⊢ x = k + 1 → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ P ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1
20 19 imbi2d ⊢ x = k + 1 → φ → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ φ → P ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1
21 fveq2 ⊢ x = N → P ⁡ x = P ⁡ N
22 fveq2 ⊢ x = N → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N
23 21 22 eqeq12d ⊢ x = N → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ P ⁡ N = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N
24 23 imbi2d ⊢ x = N → φ → P ⁡ x = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ↔ φ → P ⁡ N = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N
25 1 2 3 smup0 ⊢ φ → P ⁡ 0 = ∅
26 inss1 ⊢ A ∩ 0 ..^ N ⊆ A
27 26 1 sstrid ⊢ φ → A ∩ 0 ..^ N ⊆ ℕ 0
28 eqid ⊢ seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
29 27 2 28 smup0 ⊢ φ → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = ∅
30 25 29 eqtr4d ⊢ φ → P ⁡ 0 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
31 30 a1i ⊢ N ∈ ℤ ≥ 0 → φ → P ⁡ 0 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
32 oveq1 ⊢ P ⁡ k = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k → P ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B
33 1 adantr ⊢ φ ∧ k ∈ 0 ..^ N → A ⊆ ℕ 0
34 2 adantr ⊢ φ ∧ k ∈ 0 ..^ N → B ⊆ ℕ 0
35 elfzouz ⊢ k ∈ 0 ..^ N → k ∈ ℤ ≥ 0
36 35 adantl ⊢ φ ∧ k ∈ 0 ..^ N → k ∈ ℤ ≥ 0
37 36 5 eleqtrrdi ⊢ φ ∧ k ∈ 0 ..^ N → k ∈ ℕ 0
38 33 34 3 37 smupp1 ⊢ φ ∧ k ∈ 0 ..^ N → P ⁡ k + 1 = P ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B
39 27 adantr ⊢ φ ∧ k ∈ 0 ..^ N → A ∩ 0 ..^ N ⊆ ℕ 0
40 39 34 28 37 smupp1 ⊢ φ ∧ k ∈ 0 ..^ N → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∩ 0 ..^ N ∧ n − k ∈ B
41 elin ⊢ k ∈ A ∩ 0 ..^ N ↔ k ∈ A ∧ k ∈ 0 ..^ N
42 41 rbaib ⊢ k ∈ 0 ..^ N → k ∈ A ∩ 0 ..^ N ↔ k ∈ A
43 42 adantl ⊢ φ ∧ k ∈ 0 ..^ N → k ∈ A ∩ 0 ..^ N ↔ k ∈ A
44 43 anbi1d ⊢ φ ∧ k ∈ 0 ..^ N → k ∈ A ∩ 0 ..^ N ∧ n − k ∈ B ↔ k ∈ A ∧ n − k ∈ B
45 44 rabbidv ⊢ φ ∧ k ∈ 0 ..^ N → n ∈ ℕ 0 | k ∈ A ∩ 0 ..^ N ∧ n − k ∈ B = n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B
46 45 oveq2d ⊢ φ ∧ k ∈ 0 ..^ N → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∩ 0 ..^ N ∧ n − k ∈ B = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B
47 40 46 eqtrd ⊢ φ ∧ k ∈ 0 ..^ N → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B
48 38 47 eqeq12d ⊢ φ ∧ k ∈ 0 ..^ N → P ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1 ↔ P ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k sadd n ∈ ℕ 0 | k ∈ A ∧ n − k ∈ B
49 32 48 imbitrrid ⊢ φ ∧ k ∈ 0 ..^ N → P ⁡ k = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k → P ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1
50 49 expcom ⊢ k ∈ 0 ..^ N → φ → P ⁡ k = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k → P ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1
51 50 a2d ⊢ k ∈ 0 ..^ N → φ → P ⁡ k = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k → φ → P ⁡ k + 1 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ k + 1
52 12 16 20 24 31 51 fzind2 ⊢ N ∈ 0 … N → φ → P ⁡ N = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N
53 8 52 mpcom ⊢ φ → P ⁡ N = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N
54 inss2 ⊢ A ∩ 0 ..^ N ⊆ 0 ..^ N
55 54 a1i ⊢ φ → A ∩ 0 ..^ N ⊆ 0 ..^ N
56 4 nn0zd ⊢ φ → N ∈ ℤ
57 uzid ⊢ N ∈ ℤ → N ∈ ℤ ≥ N
58 56 57 syl ⊢ φ → N ∈ ℤ ≥ N
59 27 2 28 4 55 58 smupvallem ⊢ φ → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∩ 0 ..^ N ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N = A ∩ 0 ..^ N smul B
60 53 59 eqtrd ⊢ φ → P ⁡ N = A ∩ 0 ..^ N smul B