---

Step * of Lemma simple-converges-to

∀x:ℕ ⟶ ℝ. ∀a,c:ℝ.  ((∀n:ℕ. (|(x n) - a| ≤ ((r1/r(2^n)) * c))) ⇒ lim n→∞.x n = a)
BY
{ (Auto THEN Assert ⌜∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (((r1/r(2^n)) * c) ≤ (r1/r(k)))))])⌝⋅) }

1
.....assertion..... 
1. x : ℕ ⟶ ℝ
2. a : ℝ
3. c : ℝ
4. ∀n:ℕ. (|(x n) - a| ≤ ((r1/r(2^n)) * c))
⊢ ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (((r1/r(2^n)) * c) ≤ (r1/r(k)))))])

2
1. x : ℕ ⟶ ℝ
2. a : ℝ
3. c : ℝ
4. ∀n:ℕ. (|(x n) - a| ≤ ((r1/r(2^n)) * c))
5. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (((r1/r(2^n)) * c) ≤ (r1/r(k)))))])
⊢ lim n→∞.x n = a

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a,c:\mBbbR{}.    ((\mforall{}n:\mBbbN{}.  (|(x  n)  -  a|  \mleq{}  ((r1/r(2\^{}n))  *  c)))  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x  n  =  a)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}k:\mBbbN{}\msupplus{}.  (\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (((r1/r(2\^{}n))  *  c)  \mleq{}  (r1/r(k)))))])\mkleeneclose{}\mcdot{})

---

Home Index