---

Step * of Lemma near-root_wf

∀k:{2...}. ∀p:{p:ℤ| (0 ≤ p) ∨ (↑isOdd(k))} . ∀q,n:ℕ+.
  (near-root(k;p;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 (Assert ⌜TERMOF{near-root-rational-ext:o, \\v:l} k p q n ∈ ∃r:ℤ × ℕ+ [let a,b = r 
                                                                              in (0 ≤ p ⇐⇒ 0 ≤ a)
                                                                                 ∧ (|(r(a))/b^k 
                                                                                   - (r(p)/r(q))| < (r1/r(n)))]⌝⋅
         THENA Auto
         )
   ) }

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

---

Latex:

---

Latex:
\mforall{}k:\{2...\}.  \mforall{}p:\{p:\mBbbZ{}|  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}q,n:\mBbbN{}\msupplus{}.
    (near-root(k;p;q;n)  \mmember{}  \{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  (Assert  \mkleeneopen{}TERMOF\{near-root-rational-ext:o,  \mbackslash{}\mbackslash{}v:l\}  k  p  q  n  \mmember{}  \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)))]\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  )

---

Home Index