---

Step * of Lemma qsqrt-nonneg

∀[r:{r:ℚ| 0 ≤ r} ]. ∀[n:ℕ+].  (0 ≤ qsqrt(r;n))
BY
{ (Auto THEN Unfold `qsqrt` 0 THEN GenConclAtAddr [2] THEN Auto) }

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))])
⊢ 0 ≤ v

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `qsqrt`  0  THEN  GenConclAtAddr  [2]  THEN  Auto)

---

Home Index