---

Step * of Lemma int-dot-add-left

∀[as,bs,cs:ℤ List].  as + bs ⋅ cs ~ as ⋅ cs + bs ⋅ cs supposing ||as|| = ||bs|| ∈ ℤ
BY
{ (RepeatFor 2 (InductionOnList)
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `int-vec-add` 0⋅
   THEN Reduce 0
   THEN Reduce (-1)
   THEN Auto') }

1
1. u : ℤ
2. v : ℤ List
3. ∀[bs,cs:ℤ List].  v + bs ⋅ cs ~ v ⋅ cs + bs ⋅ cs supposing ||v|| = ||bs|| ∈ ℤ
4. u1 : ℤ
5. v1 : ℤ List
6. ∀[cs:ℤ List]. [u / v] + v1 ⋅ cs ~ [u / v] ⋅ cs + v1 ⋅ cs supposing ||[u / v]|| = ||v1|| ∈ ℤ
7. cs : ℤ List
8. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
⊢ [u + u1 / v + v1] ⋅ cs = ([u / v] ⋅ cs + [u1 / v1] ⋅ cs) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[as,bs,cs:\mBbbZ{}  List].    as  +  bs  \mcdot{}  cs  \msim{}  as  \mcdot{}  cs  +  bs  \mcdot{}  cs  supposing  ||as||  =  ||bs||


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `int-vec-add`  0\mcdot{}
  THEN  Reduce  0
  THEN  Reduce  (-1)
  THEN  Auto')

---

Home Index