---

Step * of Lemma qroot

∀k:{2...}. ∀a:{a:ℚ| (0 ≤ a) ∨ (↑isOdd(k))} . ∀n:ℕ+.  (∃q:ℚ [((0 ≤ a ⇐⇒ 0 ≤ q) ∧ |q ↑ k - a| < (1/n))])
BY
{ (Auto
   THEN DVar `a'⋅
   THEN (Assert (0 ≤ a) ∨ (↑isOdd(k)) BY
               (Unhide THEN Auto))
   THEN Thin 3
   THEN MoveToConcl (-1)
   THEN BetterRationalD 2
   THEN Auto
   THEN ThinVar `a') }

1
1. k : {2...}
2. n : ℕ+
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. ¬↑qeq(q;0)
8. (0 ≤ (p/q)) ∨ (↑isOdd(k))
⊢ ∃q@0:ℚ [((0 ≤ (p/q) ⇐⇒ 0 ≤ q@0) ∧ |q@0 ↑ k - (p/q)| < (1/n))]

---

Latex:

---

Latex:
\mforall{}k:\{2...\}.  \mforall{}a:\{a:\mBbbQ{}|  (0  \mleq{}  a)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
    (\mexists{}q:\mBbbQ{}  [((0  \mleq{}  a  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  q)  \mwedge{}  |q  \muparrow{}  k  -  a|  <  (1/n))])


By

---

Latex:
(Auto
  THEN  DVar  `a'\mcdot{}
  THEN  (Assert  (0  \mleq{}  a)  \mvee{}  (\muparrow{}isOdd(k))  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  3
  THEN  MoveToConcl  (-1)
  THEN  BetterRationalD  2
  THEN  Auto
  THEN  ThinVar  `a')

---

Home Index