---

Step * 1 of Lemma rsqrt-rless-iff


1. x : {x:ℝ| r0 ≤ x} 
2. y : {x:ℝ| r0 ≤ x} 
3. rsqrt(x) < rsqrt(y)
⊢ x < y
BY
{ (Assert rsqrt(x)^2 < rsqrt(y)^2 BY
         EAuto 2) }

1
1. x : {x:ℝ| r0 ≤ x} 
2. y : {x:ℝ| r0 ≤ x} 
3. rsqrt(x) < rsqrt(y)
4. rsqrt(x)^2 < rsqrt(y)^2
⊢ x < y

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  rsqrt(x)\^{}2  <  rsqrt(y)\^{}2  BY
              EAuto  2)

---

Home Index