---

Step * 2 1 1 2 of Lemma iproper-approx


1. y : ℝ
2. x2 : ℝ
3. (True ∧ True) ⇒ (y < x2)
4. n : ℕ+
5. (y + (r1/r(n))) ≤ x2
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. True ∧ True
⊢ (y + (r1/r(n + 1))) < x2
BY
{ (RWO "5<" 0 THENA Auto) }

1
1. y : ℝ
2. x2 : ℝ
3. (True ∧ True) ⇒ (y < x2)
4. n : ℕ+
5. (y + (r1/r(n))) ≤ x2
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. True ∧ True
⊢ (y + (r1/r(n + 1))) < (y + (r1/r(n)))

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "5<"  0  THENA  Auto)

---

Home Index