---

Step * 2 of Lemma select-int-vec-add


1. u : ℤ
2. v : ℤ List
3. ∀[bs:ℤ List]. ∀[i:ℕ].  v + bs[i] ~ v[i] + bs[i] supposing i < ||v|| ∧ i < ||bs||
4. u1 : ℤ
5. v1 : ℤ List
6. ∀[i:ℕ]. [u / v] + v1[i] ~ [u / v][i] + v1[i] supposing i < ||[u / v]|| ∧ i < ||v1||
7. i : ℕ
8. i < ||[u / v]||
9. i < ||[u1 / v1]||
⊢ [u + u1 / v + v1][i] = ([u / v][i] + [u1 / v1][i]) ∈ ℤ
BY
{ ((RWO "select-cons" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[bs:\mBbbZ{}  List].  \mforall{}[i:\mBbbN{}].    v  +  bs[i]  \msim{}  v[i]  +  bs[i]  supposing  i  <  ||v||  \mwedge{}  i  <  ||bs||
4.  u1  :  \mBbbZ{}
5.  v1  :  \mBbbZ{}  List
6.  \mforall{}[i:\mBbbN{}].  [u  /  v]  +  v1[i]  \msim{}  [u  /  v][i]  +  v1[i]  supposing  i  <  ||[u  /  v]||  \mwedge{}  i  <  ||v1||
7.  i  :  \mBbbN{}
8.  i  <  ||[u  /  v]||
9.  i  <  ||[u1  /  v1]||
\mvdash{}  [u  +  u1  /  v  +  v1][i]  =  ([u  /  v][i]  +  [u1  /  v1][i])


By

---

Latex:
((RWO  "select-cons"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index