---

Step * 1 1 of Lemma rsqrt_functionality_wrt_rleq


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index