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=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1
smupval.n ⊢φ→N∈ℕ0
Assertion smupval ⊢φ→P⁡N=A∩0..^NsmulB

Proof

Step Hyp Ref Expression
1 smupval.a ⊢φ→A⊆ℕ0
2 smupval.b ⊢φ→B⊆ℕ0
3 smupval.p ⊢P=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∧n−m∈Bn∈ℕ0⟼ifn=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→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡0
11 9 10 eqeq12d ⊢x=0→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔P⁡0=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡0
12 11 imbi2d ⊢x=0→φ→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔φ→P⁡0=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡0
13 fveq2 ⊢x=k→P⁡x=P⁡k
14 fveq2 ⊢x=k→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k
15 13 14 eqeq12d ⊢x=k→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔P⁡k=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k
16 15 imbi2d ⊢x=k→φ→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔φ→P⁡k=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k
17 fveq2 ⊢x=k+1→P⁡x=P⁡k+1
18 fveq2 ⊢x=k+1→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1
19 17 18 eqeq12d ⊢x=k+1→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔P⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1
20 19 imbi2d ⊢x=k+1→φ→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔φ→P⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1
21 fveq2 ⊢x=N→P⁡x=P⁡N
22 fveq2 ⊢x=N→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡N
23 21 22 eqeq12d ⊢x=N→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔P⁡N=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡N
24 23 imbi2d ⊢x=N→φ→P⁡x=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡x↔φ→P⁡N=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=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 ⊢seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1
29 27 2 28 smup0 ⊢φ→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡0=∅
30 25 29 eqtr4d ⊢φ→P⁡0=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡0
31 30 a1i ⊢N∈ℤ≥0→φ→P⁡0=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡0
32 oveq1 ⊢P⁡k=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k→P⁡ksaddn∈ℕ0|k∈A∧n−k∈B=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡ksaddn∈ℕ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⁡ksaddn∈ℕ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→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡ksaddn∈ℕ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→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡ksaddn∈ℕ0|k∈A∩0..^N∧n−k∈B=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡ksaddn∈ℕ0|k∈A∧n−k∈B
47 40 46 eqtrd ⊢φ∧k∈0..^N→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡ksaddn∈ℕ0|k∈A∧n−k∈B
48 38 47 eqeq12d ⊢φ∧k∈0..^N→P⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1↔P⁡ksaddn∈ℕ0|k∈A∧n−k∈B=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡ksaddn∈ℕ0|k∈A∧n−k∈B
49 32 48 imbitrrid ⊢φ∧k∈0..^N→P⁡k=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k→P⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1
50 49 expcom ⊢k∈0..^N→φ→P⁡k=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k→P⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1
51 50 a2d ⊢k∈0..^N→φ→P⁡k=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k→φ→P⁡k+1=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡k+1
52 12 16 20 24 31 51 fzind2 ⊢N∈0…N→φ→P⁡N=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡N
53 8 52 mpcom ⊢φ→P⁡N=seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=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 ⊢φ→seq0p∈𝒫ℕ0,m∈ℕ0⟼psaddn∈ℕ0|m∈A∩0..^N∧n−m∈Bn∈ℕ0⟼ifn=0∅n−1⁡N=A∩0..^NsmulB
60 53 59 eqtrd ⊢φ→P⁡N=A∩0..^NsmulB