---

Step * of Lemma rsqrt-unique

∀[x,s:{x:ℝ| r0 ≤ x} ].  s = rsqrt(x) supposing (s * s) = x
BY
{ (Auto
   THEN DSetVars
   THEN Unhide
   THEN Auto
   THEN (Assert ((rsqrt(x) * rsqrt(x)) = x) ∧ (r0 ≤ rsqrt(x)) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜rsqrt(x) = t ∈ ℝ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Auto) }

1
1. x : ℝ
2. r0 ≤ x
3. s : ℝ
4. r0 ≤ s
5. (s * s) = x
6. t : ℝ
7. (t * t) = x
8. r0 ≤ t
⊢ s = t

---

Latex:

---

Latex:
\mforall{}[x,s:\{x:\mBbbR{}|  r0  \mleq{}  x\}  ].    s  =  rsqrt(x)  supposing  (s  *  s)  =  x


By

---

Latex:
(Auto
  THEN  DSetVars
  THEN  Unhide
  THEN  Auto
  THEN  (Assert  ((rsqrt(x)  *  rsqrt(x))  =  x)  \mwedge{}  (r0  \mleq{}  rsqrt(x))  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}rsqrt(x)  =  t\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index