---

Step * 1 of Lemma rleq-iff-bdd


1. x : ℝ
2. y : ℝ
3. ∃B:ℕ. ∀n:ℕ+. ((x n) ≤ ((y n) + B))
4. y < x
⊢ False
BY
{ ((RWO "rless-iff2" (-1) THENA Auto)
   THEN (InstLemma `regular-less-iff` [⌜y⌝;⌜x⌝]⋅ THENA Auto)
   THEN (D -1 THEN (D -2 THENA (Auto THEN ParallelOp -2)))
   THEN Thin (-2)) }

1
1. x : ℝ
2. y : ℝ
3. ∃B:ℕ. ∀n:ℕ+. ((x n) ≤ ((y n) + B))
4. ∃n:ℕ+. (y n) + 4 < x n
5. ∀b:{4...}. ∃n:ℕ+. ∀m:{n...}. (y m) + b < x m
⊢ False

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  \mexists{}B:\mBbbN{}.  \mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  \mleq{}  ((y  n)  +  B))
4.  y  <  x
\mvdash{}  False


By

---

Latex:
((RWO  "rless-iff2"  (-1)  THENA  Auto)
  THEN  (InstLemma  `regular-less-iff`  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  THEN  (D  -2  THENA  (Auto  THEN  ParallelOp  -2)))
  THEN  Thin  (-2))

---

Home Index