---

Step * 1 of Lemma reals-close-or-rneq


1. K : ℕ+
2. 3 * K ∈ (r1)/K < (r(2))/K
⊢ ∃g:ℝ ⟶ ℝ ⟶ ℕ3 [(∀x,y:ℝ.
                      ((((g x y) = 1 ∈ ℤ) ⇒ ((r1/r(K)) < (y - x)))
                      ∧ (((g x y) = 2 ∈ ℤ) ⇒ ((r1/r(K)) < (x - y)))
                      ∧ (((g x y) = 0 ∈ ℤ) ⇒ (|x - y| < (r(2)/r(K))))))]
BY
{ (Assert ∀x,y:ℝ.  ((↓(r1/r(K)) < (y - x)) ∨ (↓(r1/r(K)) < (x - y)) ∨ (↓|x - y| < (r(2)/r(K)))) BY
         (Auto
          THEN (GenConclTerm ⌜rless-case((r1)/K;(r(2))/K;3 * K;|x - y|)⌝⋅ THENA Auto)
          THEN Thin (-1)
          THEN (RWO "int-rdiv-req" (-1) THENM D -1)
          THEN Auto
          THEN (RWO "rabs-difference-lower-bound" (-1) THENM D -1)
          THEN Auto
          THEN (OrRight THENM OrLeft)
          THEN Auto)) }

1
1. K : ℕ+
2. 3 * K ∈ (r1)/K < (r(2))/K
3. ∀x,y:ℝ.  ((↓(r1/r(K)) < (y - x)) ∨ (↓(r1/r(K)) < (x - y)) ∨ (↓|x - y| < (r(2)/r(K))))
⊢ ∃g:ℝ ⟶ ℝ ⟶ ℕ3 [(∀x,y:ℝ.
                      ((((g x y) = 1 ∈ ℤ) ⇒ ((r1/r(K)) < (y - x)))
                      ∧ (((g x y) = 2 ∈ ℤ) ⇒ ((r1/r(K)) < (x - y)))
                      ∧ (((g x y) = 0 ∈ ℤ) ⇒ (|x - y| < (r(2)/r(K))))))]

---

Latex:

---

Latex:

1.  K  :  \mBbbN{}\msupplus{}
2.  3  *  K  \mmember{}  (r1)/K  <  (r(2))/K
\mvdash{}  \mexists{}g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbN{}3  [(\mforall{}x,y:\mBbbR{}.
                                            ((((g  x  y)  =  1)  {}\mRightarrow{}  ((r1/r(K))  <  (y  -  x)))
                                            \mwedge{}  (((g  x  y)  =  2)  {}\mRightarrow{}  ((r1/r(K))  <  (x  -  y)))
                                            \mwedge{}  (((g  x  y)  =  0)  {}\mRightarrow{}  (|x  -  y|  <  (r(2)/r(K))))))]


By

---

Latex:
(Assert  \mforall{}x,y:\mBbbR{}.    ((\mdownarrow{}(r1/r(K))  <  (y  -  x))  \mvee{}  (\mdownarrow{}(r1/r(K))  <  (x  -  y))  \mvee{}  (\mdownarrow{}|x  -  y|  <  (r(2)/r(K))))  BY
              (Auto
                THEN  (GenConclTerm  \mkleeneopen{}rless-case((r1)/K;(r(2))/K;3  *  K;|x  -  y|)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Thin  (-1)
                THEN  (RWO  "int-rdiv-req"  (-1)  THENM  D  -1)
                THEN  Auto
                THEN  (RWO  "rabs-difference-lower-bound"  (-1)  THENM  D  -1)
                THEN  Auto
                THEN  (OrRight  THENM  OrLeft)
                THEN  Auto))

---

Home Index