---

Step * 1 1 1 1 2 of Lemma approximate-qsqrt


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
10. r : ℚ
11. (p/q) - (1/n) < r * r
12. r * r < (p/q) + (1/n)
13. 0 ≤ r
14. 0 ≤ r
15. (r * r) - (p/q) < (1/n)
⊢ -((r * r) - (p/q)) < (1/n)
BY
{ (QAdd ⌜(r * r) - (1/n)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  n  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  0  <  q
6.  \mneg{}(q  =  0)
7.  a  =  (p/q)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  0  \mleq{}  p
10.  r  :  \mBbbQ{}
11.  (p/q)  -  (1/n)  <  r  *  r
12.  r  *  r  <  (p/q)  +  (1/n)
13.  0  \mleq{}  r
14.  0  \mleq{}  r
15.  (r  *  r)  -  (p/q)  <  (1/n)
\mvdash{}  -((r  *  r)  -  (p/q))  <  (1/n)


By

---

Latex:
(QAdd  \mkleeneopen{}(r  *  r)  -  (1/n)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index