---

Step * of Lemma increasing-sequence-converges

∀x:ℕ ⟶ ℝ
  ((∀n:ℕ. ((x n) < (x (n + 1))))
  ⇒ (∃c:{2...}
       ∃m:ℕ+
        ((∀n:ℕ+. (((x (n + 1)) - x n) ≤ ((r1/r(c)) * ((x n) - x (n - 1)))))
        ∧ ((r(c) * ((x 1) - x 0)/r(c - 1)) ≤ (r1/r(m)))))
  ⇒ x n↓ as n→∞)
BY
{ (Auto THEN ExRepD) }

1
1. x : ℕ ⟶ ℝ
2. ∀n:ℕ. ((x n) < (x (n + 1)))
3. c : {2...}
4. m : ℕ+
5. ∀n:ℕ+. (((x (n + 1)) - x n) ≤ ((r1/r(c)) * ((x n) - x (n - 1))))
6. (r(c) * ((x 1) - x 0)/r(c - 1)) ≤ (r1/r(m))
⊢ x n↓ as n→∞

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
    ((\mforall{}n:\mBbbN{}.  ((x  n)  <  (x  (n  +  1))))
    {}\mRightarrow{}  (\mexists{}c:\{2...\}
              \mexists{}m:\mBbbN{}\msupplus{}
                ((\mforall{}n:\mBbbN{}\msupplus{}.  (((x  (n  +  1))  -  x  n)  \mleq{}  ((r1/r(c))  *  ((x  n)  -  x  (n  -  1)))))
                \mwedge{}  ((r(c)  *  ((x  1)  -  x  0)/r(c  -  1))  \mleq{}  (r1/r(m)))))
    {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index