---

Step * 2 of Lemma rsqrt-rneq


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


By

---

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

---

Home Index