---

Step * 1 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/q)
⊢ ∃q@0:ℚ [((0 ≤ q@0) ∧ |(q@0 * q@0) - (p/q)| < (1/n))]
BY
{ QMul ⌜q⌝ (-1)⋅ }

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@0:ℚ [((0 ≤ q@0) ∧ |(q@0 * q@0) - (p/q)| < (1/n))]

---

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/q)
\mvdash{}  \mexists{}q@0:\mBbbQ{}  [((0  \mleq{}  q@0)  \mwedge{}  |(q@0  *  q@0)  -  (p/q)|  <  (1/n))]


By

---

Latex:
QMul  \mkleeneopen{}q\mkleeneclose{}  (-1)\mcdot{}

---

Home Index