---

Step * 1 1 1 1 1 1 1 1 of Lemma shadow-vec-property

.....equality..... 
1. as : ℤ List
2. bs : ℤ List
3. i : ℕ||as||
4. ||as|| = ||bs|| ∈ ℤ
5. 0 ≤ as[i]
6. bs[i] ≤ 0
7. xs : ℤ List
8. ||xs|| = ||as|| ∈ ℤ
9. 0 ≤ as ⋅ xs
10. 0 ≤ bs ⋅ xs
11. 0 ≤ ((-1) * bs[i])
12. 0 ≤ (-1) * bs[i] * as ⋅ xs
13. 0 ≤ as[i] * bs ⋅ xs
14. 0 ≤ ((as[i] * bs + (-1) * bs[i] * as[i] * xs[i]) + as[i] * bs + (-1) * bs[i] * as\i ⋅ xs\i)
15. valueall-type(ℤ List)
⊢ as[i] * bs + (-1) * bs[i] * as[i] ~ 0
BY
{ TACTIC:(RWW "select-int-vec-add select-int-vec-mul" 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  as  :  \mBbbZ{}  List
2.  bs  :  \mBbbZ{}  List
3.  i  :  \mBbbN{}||as||
4.  ||as||  =  ||bs||
5.  0  \mleq{}  as[i]
6.  bs[i]  \mleq{}  0
7.  xs  :  \mBbbZ{}  List
8.  ||xs||  =  ||as||
9.  0  \mleq{}  as  \mcdot{}  xs
10.  0  \mleq{}  bs  \mcdot{}  xs
11.  0  \mleq{}  ((-1)  *  bs[i])
12.  0  \mleq{}  (-1)  *  bs[i]  *  as  \mcdot{}  xs
13.  0  \mleq{}  as[i]  *  bs  \mcdot{}  xs
14.  0  \mleq{}  ((as[i]  *  bs  +  (-1)  *  bs[i]  *  as[i]  *  xs[i])  +  as[i]  *  bs  +  (-1)  *  bs[i]  *  as\mbackslash{}i  \mcdot{}  xs\mbackslash{}i)
15.  valueall-type(\mBbbZ{}  List)
\mvdash{}  as[i]  *  bs  +  (-1)  *  bs[i]  *  as[i]  \msim{}  0


By

---

Latex:
TACTIC:(RWW  "select-int-vec-add  select-int-vec-mul"  0  THEN  Auto)

---

Home Index