---

Step * 2 1 1 4 of Lemma iproper-approx


1. y1 : ℝ
2. y : ℝ
3. (True ∧ True) ⇒ (y1 < y)
4. n : ℕ+
5. (y1 + (r1/r(n))) ≤ (y - (r1/r(n)))
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. True ∧ True
⊢ (y1 + (r1/r(n + 1))) < (y - (r1/r(n + 1)))
BY
{ (RepeatFor 2 (MoveToConcl (-3)) THEN GenConclTerms Auto [⌜(r1/r(n + 1))⌝;⌜(r1/r(n))⌝]⋅ THEN All Thin) }

1
1. y1 : ℝ
2. y : ℝ
3. v : ℝ
4. v1 : ℝ
⊢ ((y1 + v1) ≤ (y - v1)) ⇒ (v < v1) ⇒ ((y1 + v) < (y - v))

---

Latex:

---

Latex:

1.  y1  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  (True  \mwedge{}  True)  {}\mRightarrow{}  (y1  <  y)
4.  n  :  \mBbbN{}\msupplus{}
5.  (y1  +  (r1/r(n)))  \mleq{}  (y  -  (r1/r(n)))
6.  (r1/r(n  +  1))  <  (r1/r(n))
7.  r(n)  <  r(n  +  1)
8.  True  \mwedge{}  True
\mvdash{}  (y1  +  (r1/r(n  +  1)))  <  (y  -  (r1/r(n  +  1)))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-3))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}(r1/r(n  +  1))\mkleeneclose{};\mkleeneopen{}(r1/r(n))\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index