---

Step * of Lemma rleq-iff-bdd

∀[x,y:ℝ].  (x ≤ y ⇐⇒ ∃B:ℕ. ∀n:ℕ+. ((x n) ≤ ((y n) + B)))
BY
{ (Auto THENL [(RWO  "rleq-iff4" (-1) THEN Auto); ((BLemma `rleq-iff-not-rless` THEN Auto) THEN (D 0 THENA Auto))]) }

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

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (x  \mleq{}  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}B:\mBbbN{}.  \mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  \mleq{}  ((y  n)  +  B)))


By

---

Latex:
(Auto
  THENL  [(RWO    "rleq-iff4"  (-1)  THEN  Auto)
              ;  ((BLemma  `rleq-iff-not-rless`  THEN  Auto)  THEN  (D  0  THENA  Auto))]
)

---

Home Index