---

Step * of Lemma sign-absval

∀[x:ℤ]. ((sign(x) * |x|) = x ∈ ℤ)
BY
{ (Auto THEN Unfolds ``sign`` 0 THEN (RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  ((sign(x)  *  |x|)  =  x)


By

---

Latex:
(Auto  THEN  Unfolds  ``sign``  0  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index