---

Step * 1 2 of Lemma increasing-sequence-converges


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))
7. ∀n:ℕ+. (((x (n + 1)) - x n) ≤ ((r1/r(c^n)) * ((x 1) - x 0)))
⊢ x n↓ as n→∞
BY
{ ((Assert r0 < ((x 1) - x 0) BY
          (nRAdd ⌜x 0⌝ 0⋅ THEN Auto))
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN Thin (-1)
   THEN RenameVar `M' (-1)
   THEN ((GenConclTerm ⌜(x 1) - x 0⌝⋅ THENA Auto) THEN Thin (-1))
   THEN Auto) }

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

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  \mforall{}n:\mBbbN{}.  ((x  n)  <  (x  (n  +  1)))
3.  c  :  \{2...\}
4.  m  :  \mBbbN{}\msupplus{}
5.  \mforall{}n:\mBbbN{}\msupplus{}.  (((x  (n  +  1))  -  x  n)  \mleq{}  ((r1/r(c))  *  ((x  n)  -  x  (n  -  1))))
6.  (r(c)  *  ((x  1)  -  x  0)/r(c  -  1))  \mleq{}  (r1/r(m))
7.  \mforall{}n:\mBbbN{}\msupplus{}.  (((x  (n  +  1))  -  x  n)  \mleq{}  ((r1/r(c\^{}n))  *  ((x  1)  -  x  0)))
\mvdash{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{}


By

---

Latex:
((Assert  r0  <  ((x  1)  -  x  0)  BY
                (nRAdd  \mkleeneopen{}x  0\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  Thin  (-1)
  THEN  RenameVar  `M'  (-1)
  THEN  ((GenConclTerm  \mkleeneopen{}(x  1)  -  x  0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1))
  THEN  Auto)

---

Home Index