---

Step * of Lemma rroot-exists

∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} .  (∃y:{ℝ| (((↑isEven(i)) ⇒ (r0 ≤ y)) ∧ (y^i = x))})
BY
{ (InstLemma `rroot-exists1-ext` []
   THEN RepeatFor 2 (ParallelLast')
   THEN ExRepD
   THEN (Assert q n↓ as n→∞ BY
               (FLemma `rroot-exists-part2` [-1]⋅ THEN Auto THEN FLemma `converges-iff-cauchy` [-1]⋅ THEN Auto))
   THEN D -1
   THEN With ⌜y⌝ (D 0)⋅
   THEN Auto) }

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. lim n→∞.q n^i = x
5. y : ℝ
6. lim n→∞.q n = y
7. ↑isEven(i)
⊢ r0 ≤ y

2
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. lim n→∞.q n^i = x
5. y : ℝ
6. lim n→∞.q n = y
7. (↑isEven(i)) ⇒ (r0 ≤ y)
⊢ y^i = x

---

Latex:

---

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  .    (\mexists{}y:\{\mBbbR{}|  (((\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  y))  \mwedge{}  (y\^{}i  =  x))\})


By

---

Latex:
(InstLemma  `rroot-exists1-ext`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  ExRepD
  THEN  (Assert  q  n\mdownarrow{}  as  n\mrightarrow{}\minfty{}  BY
                          (FLemma  `rroot-exists-part2`  [-1]\mcdot{}
                            THEN  Auto
                            THEN  FLemma  `converges-iff-cauchy`  [-1]\mcdot{}
                            THEN  Auto))
  THEN  D  -1
  THEN  With  \mkleeneopen{}y\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index