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