---

Step * of Lemma near-root-rational

No Annotations
∀k:{2...}. ∀p:{p:ℤ| (0 ≤ p) ∨ (↑isOdd(k))} . ∀q,n:ℕ+.
  (∃r:ℤ × ℕ+ [let a,b = r 
              in (0 ≤ p ⇐⇒ 0 ≤ a) ∧ (|(r(a))/b^k - (r(p)/r(q))| < (r1/r(n)))])
BY
{ (Auto THEN D 2 THEN (Assert (0 ≤ p) ∨ (↑isOdd(k)) BY (Unhide THEN Auto)) THEN Thin 3) }

1
1. k : {2...}
2. p : ℤ
3. q : ℕ+
4. n : ℕ+
5. (0 ≤ p) ∨ (↑isOdd(k))
⊢ ∃r:ℤ × ℕ+ [let a,b = r 
             in (0 ≤ p ⇐⇒ 0 ≤ a) ∧ (|(r(a))/b^k - (r(p)/r(q))| < (r1/r(n)))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\{2...\}.  \mforall{}p:\{p:\mBbbZ{}|  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}q,n:\mBbbN{}\msupplus{}.
    (\mexists{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  [let  a,b  =  r 
                            in  (0  \mleq{}  p  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  a)  \mwedge{}  (|(r(a))/b\^{}k  -  (r(p)/r(q))|  <  (r1/r(n)))])


By

---

Latex:
(Auto  THEN  D  2  THEN  (Assert  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))  BY  (Unhide  THEN  Auto))  THEN  Thin  3)

---

Home Index