---

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


1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. q : ℕ ⟶ ℝ
4. (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0)))) ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))
5. h : k:ℕ+ ⟶ ℕ
6. ∀k:ℕ+. ∀n:ℕ.  (((h k) ≤ n) ⇒ (|q n^i - x| ≤ (r1/r(k))))
7. k : ℕ+
8. k^i ∈ ℕ+
9. 2 * k^i ∈ ℕ+
10. n : ℕ
11. m : ℕ
12. (h (2 * k^i)) ≤ n
13. (h (2 * k^i)) ≤ m
14. |q n^i - q m^i| ≤ (r1/r(k^i))
15. ((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))
⊢ |(q n) - q m| ≤ (r1/r(k))
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConclAtAddr [2;2;1;1;1] THEN RenameVar `a' (-2))
   THEN GenConclAtAddr [2;2;1;1;2]
   THEN RenameVar `b' (-2)
   THEN All Thin
   THEN Auto)⋅ }

1
1. i : {2...}
2. k : ℕ+
3. a : ℝ
4. b : ℝ
5. |a^i - b^i| ≤ (r1/r(k^i))
6. ((r0 ≤ a) ∧ (r0 ≤ b)) ∨ ((a ≤ r0) ∧ (b ≤ r0))
⊢ |a - b| ≤ (r1/r(k))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclAtAddr  [2;2;1;1;1]  THEN  RenameVar  `a'  (-2))
  THEN  GenConclAtAddr  [2;2;1;1;2]
  THEN  RenameVar  `b'  (-2)
  THEN  All  Thin
  THEN  Auto)\mcdot{}

---

Home Index