Step
*
of Lemma
rsqrt_square
∀[x:ℝ]. (rsqrt(x * x) = |x|)
BY
{ (Auto
THEN (Assert (x * x) = (|x| * |x|) BY
(RWO "rabs-rmul<" 0 THEN Auto THEN RWO "rabs-of-nonneg" 0 THEN Auto))
THEN RWO "-1" 0
THEN Auto) }
Latex:
Latex:
\mforall{}[x:\mBbbR{}]. (rsqrt(x * x) = |x|)
By
Latex:
(Auto
THEN (Assert (x * x) = (|x| * |x|) BY
(RWO "rabs-rmul<" 0 THEN Auto THEN RWO "rabs-of-nonneg" 0 THEN Auto))
THEN RWO "-1" 0
THEN Auto)
Home
Index