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