---

Step * of Lemma qsqrt-property

∀[r:{r:ℚ| 0 ≤ r} ]. ∀[n:ℕ+].  |(qsqrt(r;n) * qsqrt(r;n)) - r| < (1/n)
BY
{ xxx(Auto THEN Unfold `qsqrt` 0 THEN GenConclAtAddr [1;1;1;1] THEN Auto)xxx }

1
1. r : {r:ℚ| 0 ≤ r} 
2. n : ℕ+
3. v : ∃q:ℚ [((0 ≤ q) ∧ |(q * q) - r| < (1/n))]
4. (TERMOF{approximate-qsqrt-ext:o, 1:l} r n) = v ∈ (∃q:ℚ [((0 ≤ q) ∧ |(q * q) - r| < (1/n))])
⊢ |(v * v) - r| < (1/n)

---

Latex:

---

Latex:
\mforall{}[r:\{r:\mBbbQ{}|  0  \mleq{}  r\}  ].  \mforall{}[n:\mBbbN{}\msupplus{}].    |(qsqrt(r;n)  *  qsqrt(r;n))  -  r|  <  (1/n)


By

---

Latex:
xxx(Auto  THEN  Unfold  `qsqrt`  0  THEN  GenConclAtAddr  [1;1;1;1]  THEN  Auto)xxx

---

Home Index