---

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