---

Step * of Lemma approximate-qsqrt

No Annotations
∀a:{a:ℚ| 0 ≤ a} . ∀n:ℕ+.  (∃q:ℚ [((0 ≤ q) ∧ |(q * q) - a| < (1/n))])
BY
{ (Auto
   THEN D 1
   THEN (Assert 0 ≤ a BY
               (Unhide THEN Auto))
   THEN Thin 2
   THEN MoveToConcl (-1)
   THEN BetterRationalD 1
   THEN Auto) }

1
1. a : ℚ
2. n : ℕ+
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. a = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. 0 ≤ (p/q)
⊢ ∃q@0:ℚ [((0 ≤ q@0) ∧ |(q@0 * q@0) - (p/q)| < (1/n))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:\{a:\mBbbQ{}|  0  \mleq{}  a\}  .  \mforall{}n:\mBbbN{}\msupplus{}.    (\mexists{}q:\mBbbQ{}  [((0  \mleq{}  q)  \mwedge{}  |(q  *  q)  -  a|  <  (1/n))])


By

---

Latex:
(Auto
  THEN  D  1
  THEN  (Assert  0  \mleq{}  a  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  2
  THEN  MoveToConcl  (-1)
  THEN  BetterRationalD  1
  THEN  Auto)

---

Home Index