---

Step * 1 of Lemma int-dot-add-left


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) ∈ ℤ
BY
{ ((D -2 THEN Reduce 0) THEN Auto THEN RWO "3" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((D  -2  THEN  Reduce  0)  THEN  Auto  THEN  RWO  "3"  0  THEN  Auto)

---

Home Index