---

Step * 1 of Lemma near-root_wf


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)))} 
BY
{ (RW (AddrC [2] (TagC (mk_tag_term 5))) (-1) THEN Trivial) }

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  p  :  \{p:\mBbbZ{}|  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))\} 
3.  q  :  \mBbbN{}\msupplus{}
4.  n  :  \mBbbN{}\msupplus{}
5.  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)))]
\mvdash{}  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:
(RW  (AddrC  [2]  (TagC  (mk\_tag\_term  5)))  (-1)  THEN  Trivial)

---

Home Index