---

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


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 ≤ ((0 * xs[i]) + as[i] * bs + (-1) * bs[i] * as\i ⋅ xs\i)
15. valueall-type(ℤ List)
⊢ 0 ≤ as[i] * bs + -bs[i] * as\i ⋅ xs\i
BY
{ TACTIC:(All (RW IntNormC)  THEN Auto) }

---

Latex:

---

Latex:

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{}  ((0  *  xs[i])  +  as[i]  *  bs  +  (-1)  *  bs[i]  *  as\mbackslash{}i  \mcdot{}  xs\mbackslash{}i)
15.  valueall-type(\mBbbZ{}  List)
\mvdash{}  0  \mleq{}  as[i]  *  bs  +  -bs[i]  *  as\mbackslash{}i  \mcdot{}  xs\mbackslash{}i


By

---

Latex:
TACTIC:(All  (RW  IntNormC)    THEN  Auto)

---

Home Index