---

Step * of Lemma rneq-if-rabs2

∀x,y:ℝ.  ((r0 < |x - y|) ⇒ x ≠ y)
BY
{ (Auto
   THEN D -1
   THEN (Assert (r0 n) + 4 < |x - y| n BY
               Auto)
   THEN Thin (-2)
   THEN (Subst' (r0 n) + 4 ~ 4 -1 THENA (Computation THEN Auto))) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. 4 < |x - y| n
⊢ x ≠ y

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((r0  <  |x  -  y|)  {}\mRightarrow{}  x  \mneq{}  y)


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (Assert  (r0  n)  +  4  <  |x  -  y|  n  BY
                          Auto)
  THEN  Thin  (-2)
  THEN  (Subst'  (r0  n)  +  4  \msim{}  4  -1  THENA  (Computation  THEN  Auto)))

---

Home Index