---

Step * of Lemma rneq-if-rabs

∀x,y:ℝ.  x ≠ y supposing r0 < |x - y|
BY
{ TACTIC:(Auto
          THEN (Assert ∃n:ℕ+. 4 < |x - y| n BY
                      ((D 0 With ⌜rlessw(r0;|x - y|)⌝  THEN Auto)
                       THEN (GenConclTerm ⌜rlessw(r0;|x - y|)⌝⋅ THENA Auto)
                       THEN Thin (-1)
                       THEN D -1
                       THEN RepUR ``int-to-real`` -1
                       THEN Auto))
          THEN Thin (-2)
          THEN ExRepD) }

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

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  (Assert  \mexists{}n:\mBbbN{}\msupplus{}.  4  <  |x  -  y|  n  BY
                                        ((D  0  With  \mkleeneopen{}rlessw(r0;|x  -  y|)\mkleeneclose{}    THEN  Auto)
                                          THEN  (GenConclTerm  \mkleeneopen{}rlessw(r0;|x  -  y|)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                          THEN  Thin  (-1)
                                          THEN  D  -1
                                          THEN  RepUR  ``int-to-real``  -1
                                          THEN  Auto))
                THEN  Thin  (-2)
                THEN  ExRepD)

---

Home Index