---

Step * 2 of Lemma sup-unique


1. A : Set(ℝ)
2. b : ℝ
3. c : ℝ
4. A ≤ b
5. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ ((b - e) < x))))
6. A ≤ c
7. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ ((c - e) < x))))
8. k : ℕ+
9. (b - c) ≤ (r1/r(k))
⊢ -(b - c) ≤ (r1/r(k))
BY
{ (((InstHyp [⌜(r1/r(k))⌝] 7)⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert x ≤ b BY
               Auto)
   THEN nRAdd ⌜b - (r1/r(k))⌝ 0⋅
   THEN nRNorm (-2)
   THEN RelRST
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Set(\mBbbR{})
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  A  \mleq{}  b
5.  \mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  A)  \mwedge{}  ((b  -  e)  <  x))))
6.  A  \mleq{}  c
7.  \mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  A)  \mwedge{}  ((c  -  e)  <  x))))
8.  k  :  \mBbbN{}\msupplus{}
9.  (b  -  c)  \mleq{}  (r1/r(k))
\mvdash{}  -(b  -  c)  \mleq{}  (r1/r(k))


By

---

Latex:
(((InstHyp  [\mkleeneopen{}(r1/r(k))\mkleeneclose{}]  7)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  x  \mleq{}  b  BY
                          Auto)
  THEN  nRAdd  \mkleeneopen{}b  -  (r1/r(k))\mkleeneclose{}  0\mcdot{}
  THEN  nRNorm  (-2)
  THEN  RelRST
  THEN  Auto)

---

Home Index