---

Step * 1 1 of Lemma rsqrt-rless-iff


1. x : {x:ℝ| r0 ≤ x} 
2. y : {x:ℝ| r0 ≤ x} 
3. rsqrt(x) < rsqrt(y)
4. rsqrt(x)^2 < rsqrt(y)^2
⊢ x < y
BY
{ (RWO  "rsqrt-rnexp-2" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  r0  \mleq{}  x\} 
2.  y  :  \{x:\mBbbR{}|  r0  \mleq{}  x\} 
3.  rsqrt(x)  <  rsqrt(y)
4.  rsqrt(x)\^{}2  <  rsqrt(y)\^{}2
\mvdash{}  x  <  y


By

---

Latex:
(RWO    "rsqrt-rnexp-2"  (-1)  THEN  Auto)

---

Home Index