---

Step * of Lemma absval_neg

∀[i:{...0}]. (|i| = (-i) ∈ ℤ)
BY
{ (Auto THEN RWO "absval_unfold" 0 THEN Auto THEN AutoSplit THEN Auto') }

1
1. i : {...0}
2. -1 < i
⊢ i = (-i) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[i:\{...0\}].  (|i|  =  (-i))


By

---

Latex:
(Auto  THEN  RWO  "absval\_unfold"  0  THEN  Auto  THEN  AutoSplit  THEN  Auto')

---

Home Index