---

Step * 1 of Lemma rsqrt-rneq


1. x : {x:ℝ| r0 ≤ x} 
2. y : {x:ℝ| r0 ≤ x} 
3. rsqrt(x) < rsqrt(y)
⊢ x < y
BY
{ ((InstLemma `rnexp-rless` [⌜rsqrt(x)⌝;⌜rsqrt(y)⌝;⌜2⌝]⋅ THENA Auto) THEN 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)
\mvdash{}  x  <  y


By

---

Latex:
((InstLemma  `rnexp-rless`  [\mkleeneopen{}rsqrt(x)\mkleeneclose{};\mkleeneopen{}rsqrt(y)\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "rsqrt-rnexp-2"  (-1)
  THEN  Auto)

---

Home Index