---

Step * 1 1 1 1 1 2 of Lemma absval_strict_ubound


1. i : ℤ
2. -1 < i
3. 0 ≤ i
⊢ ((-1) * i) ≤ i
BY
{ (Mul ⌜2⌝ (-1)⋅ THEN Add ⌜-i⌝ (-1)⋅) }

1
1. i : ℤ
2. -1 < i
3. 0 ≤ i
4. (2 * 0) ≤ (2 * i)
5. ((2 * 0) + (-i)) ≤ ((2 * i) + (-i))
⊢ ((-1) * i) ≤ i

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  -1  <  i
3.  0  \mleq{}  i
\mvdash{}  ((-1)  *  i)  \mleq{}  i


By

---

Latex:
(Mul  \mkleeneopen{}2\mkleeneclose{}  (-1)\mcdot{}  THEN  Add  \mkleeneopen{}-i\mkleeneclose{}  (-1)\mcdot{})

---

Home Index