---

Step * 1 of Lemma rleq-iff4


1. x : ℝ
2. y : ℝ
3. x ≤ y@i
4. n : ℕ+@i
⊢ (x n) ≤ ((y n) + 4)
BY
{ (((SupposeNot THENA Auto) THEN Assert ⌜False⌝⋅ THEN Auto)
   THEN (Assert y < x BY
               (With ⌜n⌝ (D 0)⋅ THEN Auto))
   THEN (RWO "rless-iff-large-diff" (-1) THENA Auto)
   THEN (InstHyp [⌜12⌝] (-1)⋅ THENA Auto)
   THEN ExRepD) }

1
1. x : ℝ
2. y : ℝ
3. x ≤ y@i
4. n : ℕ+@i
5. ¬((x n) ≤ ((y n) + 4))
6. ∀b:ℕ+. ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (b ≤ ((x m) - y m)))
7. n1 : ℕ+
8. ∀m:ℕ+. ((n1 ≤ m) ⇒ (12 ≤ ((x m) - y m)))
⊢ False

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  x  \mleq{}  y@i
4.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  (x  n)  \mleq{}  ((y  n)  +  4)


By

---

Latex:
(((SupposeNot  THENA  Auto)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  y  <  x  BY
                          (With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  (RWO  "rless-iff-large-diff"  (-1)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}12\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index