---

Step * 1 1 of Lemma rsqrt-as-rexp


1. x : {x:ℝ| r0 < x} 
2. ∀[s:{x:ℝ| r0 ≤ x} ]. s = rsqrt(x) supposing (s * s) = x
3. r0 < e^(rlog(x)/r(2))
4. ((rlog(x)/r(2)) + (rlog(x)/r(2))) = rlog(x)
⊢ e^(rlog(x)/r(2)) + (rlog(x)/r(2)) = x
BY
{ (RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  r0  <  x\} 
2.  \mforall{}[s:\{x:\mBbbR{}|  r0  \mleq{}  x\}  ].  s  =  rsqrt(x)  supposing  (s  *  s)  =  x
3.  r0  <  e\^{}(rlog(x)/r(2))
4.  ((rlog(x)/r(2))  +  (rlog(x)/r(2)))  =  rlog(x)
\mvdash{}  e\^{}(rlog(x)/r(2))  +  (rlog(x)/r(2))  =  x


By

---

Latex:
(RWO  "-1"  0  THEN  Auto)

---

Home Index