Step * of Lemma sign-absval

[x:ℤ]. ((sign(x) |x|) x ∈ ℤ)
BY
(Auto THEN Unfolds ``sign`` THEN (RWO "absval_unfold" 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