---

Step * 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))
⊢ (e^(rlog(x)/r(2)) * e^(rlog(x)/r(2))) = x
BY
{ ((RWO "rexp-radd<" 0 THENA Auto)
   THEN (Assert ⌜((rlog(x)/r(2)) + (rlog(x)/r(2))) = rlog(x)⌝⋅ THENA (nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
   ) }

1
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

---

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))
\mvdash{}  (e\^{}(rlog(x)/r(2))  *  e\^{}(rlog(x)/r(2)))  =  x


By

---

Latex:
((RWO  "rexp-radd<"  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}((rlog(x)/r(2))  +  (rlog(x)/r(2)))  =  rlog(x)\mkleeneclose{}\mcdot{}  THENA  (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  )

---

Home Index