---

Step * 2 1 1 8 of Lemma iproper-approx


1. y1 : ℝ
2. y : Top
3. iproper(<inl (inr y1 ), inr y >)
4. n : ℕ+
5. (y1 + (r1/r(n))) ≤ r(n)
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. i-finite([y1 + (r1/r(n + 1)), r(n + 1)])
⊢ (y1 + (r1/r(n + 1))) < r(n + 1)
BY
{ (Assert (y1 + (r1/r(n + 1))) < (y1 + (r1/r(n))) BY
         (nRAdd ⌜-(y1)⌝ 0⋅ THEN Auto)) }

1
1. y1 : ℝ
2. y : Top
3. iproper(<inl (inr y1 ), inr y >)
4. n : ℕ+
5. (y1 + (r1/r(n))) ≤ r(n)
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. i-finite([y1 + (r1/r(n + 1)), r(n + 1)])
9. (y1 + (r1/r(n + 1))) < (y1 + (r1/r(n)))
⊢ (y1 + (r1/r(n + 1))) < r(n + 1)

---

Latex:

---

Latex:

1.  y1  :  \mBbbR{}
2.  y  :  Top
3.  iproper(<inl  (inr  y1  ),  inr  y  >)
4.  n  :  \mBbbN{}\msupplus{}
5.  (y1  +  (r1/r(n)))  \mleq{}  r(n)
6.  (r1/r(n  +  1))  <  (r1/r(n))
7.  r(n)  <  r(n  +  1)
8.  i-finite([y1  +  (r1/r(n  +  1)),  r(n  +  1)])
\mvdash{}  (y1  +  (r1/r(n  +  1)))  <  r(n  +  1)


By

---

Latex:
(Assert  (y1  +  (r1/r(n  +  1)))  <  (y1  +  (r1/r(n)))  BY
              (nRAdd  \mkleeneopen{}-(y1)\mkleeneclose{}  0\mcdot{}  THEN  Auto))

---

Home Index