---

Step * 1 1 1 2 of Lemma rroot-exists-part2


1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. q : {q:ℕ ⟶ ℝ| 
        (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
        ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))} 
4. h : k:ℕ+ ⟶ ℕ
5. ∀k:ℕ+. ∀n:ℕ.  (((h k) ≤ n) ⇒ (|q n^i - x| ≤ (r1/r(k))))
6. k : ℕ+
7. k^i ∈ ℕ+
8. 2 * k^i ∈ ℕ+
9. n : ℕ
10. m : ℕ
11. (h (2 * k^i)) ≤ n
12. (h (2 * k^i)) ≤ m
13. ¬(k^i = 0 ∈ ℤ)
⊢ |q n^i - q m^i| ≤ (r1/r(k^i))
BY
{ ((InstHyp [⌜2 * k^i⌝;⌜n⌝] 5⋅ THENA Auto)
   THEN InstHyp [⌜2 * k^i⌝;⌜m⌝] 5⋅
   THEN Auto
   THEN InstLemma `r-triangle-inequality2` [⌜q n^i⌝;⌜x⌝;⌜q m^i⌝]⋅
   THEN Auto
   THEN RWO "-1" 0
   THEN Auto
   THEN Thin (-1))⋅ }

1
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. q : {q:ℕ ⟶ ℝ| 
        (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
        ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))} 
4. h : k:ℕ+ ⟶ ℕ
5. ∀k:ℕ+. ∀n:ℕ.  (((h k) ≤ n) ⇒ (|q n^i - x| ≤ (r1/r(k))))
6. k : ℕ+
7. k^i ∈ ℕ+
8. 2 * k^i ∈ ℕ+
9. n : ℕ
10. m : ℕ
11. (h (2 * k^i)) ≤ n
12. (h (2 * k^i)) ≤ m
13. ¬(k^i = 0 ∈ ℤ)
14. |q n^i - x| ≤ (r1/r(2 * k^i))
15. |q m^i - x| ≤ (r1/r(2 * k^i))
⊢ (|q n^i - x| + |x - q m^i|) ≤ (r1/r(k^i))

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\} 
3.  q  :  \{q:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}| 
                (\mforall{}n,m:\mBbbN{}.    (((r0  \mleq{}  (q  n))  \mwedge{}  (r0  \mleq{}  (q  m)))  \mvee{}  (((q  n)  \mleq{}  r0)  \mwedge{}  ((q  m)  \mleq{}  r0))))
                \mwedge{}  ((\muparrow{}isEven(i))  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  (r0  \mleq{}  (q  m))))\} 
4.  h  :  k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}
5.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.    (((h  k)  \mleq{}  n)  {}\mRightarrow{}  (|q  n\^{}i  -  x|  \mleq{}  (r1/r(k))))
6.  k  :  \mBbbN{}\msupplus{}
7.  k\^{}i  \mmember{}  \mBbbN{}\msupplus{}
8.  2  *  k\^{}i  \mmember{}  \mBbbN{}\msupplus{}
9.  n  :  \mBbbN{}
10.  m  :  \mBbbN{}
11.  (h  (2  *  k\^{}i))  \mleq{}  n
12.  (h  (2  *  k\^{}i))  \mleq{}  m
13.  \mneg{}(k\^{}i  =  0)
\mvdash{}  |q  n\^{}i  -  q  m\^{}i|  \mleq{}  (r1/r(k\^{}i))


By

---

Latex:
((InstHyp  [\mkleeneopen{}2  *  k\^{}i\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}2  *  k\^{}i\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  5\mcdot{}
  THEN  Auto
  THEN  InstLemma  `r-triangle-inequality2`  [\mkleeneopen{}q  n\^{}i\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}q  m\^{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  Thin  (-1))\mcdot{}

---

Home Index