---

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


1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. ∀k:ℕ+
     ∃q:ℝ
      ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
4. q : k:ℕ+ ⟶ ℝ
5. ∀k:ℕ+
     ((|q k^i - x| ≤ (r1/r(k)))
     ∧ ((r0 < (q k)) ⇒ (r0 < x))
     ∧ (((q k) < r0) ⇒ (x < r0))
     ∧ ((r0 < (q k)) ∨ ((q k) < r0) ∨ ((q k) = r0)))
6. lim n→∞.(λn.(q (n + 1))) n^i = x
7. n : ℕ
8. m : ℕ
⊢ ((r0 ≤ ((λn.(q (n + 1))) n)) ∧ (r0 ≤ ((λn.(q (n + 1))) m)))
∨ ((((λn.(q (n + 1))) n) ≤ r0) ∧ (((λn.(q (n + 1))) m) ≤ r0))
BY
{ TACTIC:TACTIC:(All Reduce THEN Auto THEN InstHyp [⌜m + 1⌝] (-4)⋅ THEN Auto THEN D -1 THEN Auto) }

1
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. ∀k:ℕ+
     ∃q:ℝ
      ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
4. q : k:ℕ+ ⟶ ℝ
5. ∀k:ℕ+
     ((|q k^i - x| ≤ (r1/r(k)))
     ∧ ((r0 < (q k)) ⇒ (r0 < x))
     ∧ (((q k) < r0) ⇒ (x < r0))
     ∧ ((r0 < (q k)) ∨ ((q k) < r0) ∨ ((q k) = r0)))
6. lim n→∞.q (n + 1)^i = x
7. n : ℕ
8. m : ℕ
9. |q (m + 1)^i - x| ≤ (r1/r(m + 1))
10. ((q (m + 1)) < r0) ⇒ (x < r0)
11. r0 < (q (m + 1))
12. r0 < x
⊢ ((r0 ≤ (q (n + 1))) ∧ (r0 ≤ (q (m + 1)))) ∨ (((q (n + 1)) ≤ r0) ∧ ((q (m + 1)) ≤ r0))

2
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. ∀k:ℕ+
     ∃q:ℝ
      ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
4. q : k:ℕ+ ⟶ ℝ
5. ∀k:ℕ+
     ((|q k^i - x| ≤ (r1/r(k)))
     ∧ ((r0 < (q k)) ⇒ (r0 < x))
     ∧ (((q k) < r0) ⇒ (x < r0))
     ∧ ((r0 < (q k)) ∨ ((q k) < r0) ∨ ((q k) = r0)))
6. lim n→∞.q (n + 1)^i = x
7. n : ℕ
8. m : ℕ
9. |q (m + 1)^i - x| ≤ (r1/r(m + 1))
10. (r0 < (q (m + 1))) ⇒ (r0 < x)
11. ((q (m + 1)) < r0) ⇒ (x < r0)
12. ((q (m + 1)) < r0) ∨ ((q (m + 1)) = r0)
⊢ ((r0 ≤ (q (n + 1))) ∧ (r0 ≤ (q (m + 1)))) ∨ (((q (n + 1)) ≤ r0) ∧ ((q (m + 1)) ≤ r0))

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\} 
3.  \mforall{}k:\mBbbN{}\msupplus{}
          \mexists{}q:\mBbbR{}
            ((|q\^{}i  -  x|  \mleq{}  (r1/r(k)))
            \mwedge{}  ((r0  <  q)  {}\mRightarrow{}  (r0  <  x))
            \mwedge{}  ((q  <  r0)  {}\mRightarrow{}  (x  <  r0))
            \mwedge{}  ((r0  <  q)  \mvee{}  (q  <  r0)  \mvee{}  (q  =  r0)))
4.  q  :  k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbR{}
5.  \mforall{}k:\mBbbN{}\msupplus{}
          ((|q  k\^{}i  -  x|  \mleq{}  (r1/r(k)))
          \mwedge{}  ((r0  <  (q  k))  {}\mRightarrow{}  (r0  <  x))
          \mwedge{}  (((q  k)  <  r0)  {}\mRightarrow{}  (x  <  r0))
          \mwedge{}  ((r0  <  (q  k))  \mvee{}  ((q  k)  <  r0)  \mvee{}  ((q  k)  =  r0)))
6.  lim  n\mrightarrow{}\minfty{}.(\mlambda{}n.(q  (n  +  1)))  n\^{}i  =  x
7.  n  :  \mBbbN{}
8.  m  :  \mBbbN{}
\mvdash{}  ((r0  \mleq{}  ((\mlambda{}n.(q  (n  +  1)))  n))  \mwedge{}  (r0  \mleq{}  ((\mlambda{}n.(q  (n  +  1)))  m)))
\mvee{}  ((((\mlambda{}n.(q  (n  +  1)))  n)  \mleq{}  r0)  \mwedge{}  (((\mlambda{}n.(q  (n  +  1)))  m)  \mleq{}  r0))


By

---

Latex:
TACTIC:TACTIC:(All  Reduce  THEN  Auto  THEN  InstHyp  [\mkleeneopen{}m  +  1\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto  THEN  D  -1  THEN  Auto)

---

Home Index