---

Step * 1 1 1 1 1 2 1 of Lemma absval_strict_ubound


1. i : ℤ
2. -1 < i
3. 0 ≤ i
4. (2 * 0) ≤ (2 * i)
5. ((2 * 0) + (-i)) ≤ ((2 * i) + (-i))
⊢ ((-1) * i) ≤ i
BY
{ (RW IntNormC (-1) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RW  IntNormC  (-1)  THEN  Auto)

---

Home Index