---

Step * of Lemma req-iff-rabs-rleq-bound

∀x,y:ℝ.  (x = y ⇐⇒ ∃B:ℕ+. ∀m:ℕ+. (|x - y| ≤ (r(B)/r(m))))
BY
{ (InstLemma `req-iff-rabs-rleq` [] THEN RepeatFor 3 ((ParallelLast' THENA Auto))) }

1
1. x : ℝ
2. y : ℝ
3. x = y
4. ∀m:ℕ+. (|x - y| ≤ (r1/r(m)))
⊢ ∃B:ℕ+. ∀m:ℕ+. (|x - y| ≤ (r(B)/r(m)))

2
1. x : ℝ
2. y : ℝ
3. ∃B:ℕ+. ∀m:ℕ+. (|x - y| ≤ (r(B)/r(m)))
4. m : ℕ+
⊢ |x - y| ≤ (r1/r(m))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}B:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbN{}\msupplus{}.  (|x  -  y|  \mleq{}  (r(B)/r(m))))


By

---

Latex:
(InstLemma  `req-iff-rabs-rleq`  []  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto)))

---

Home Index