---

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


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))))))]
BY
{ (RenameVar `f' (-1)
   THEN D 0 With ⌜λx,y. case f x y of inl(_) => 1 | inr(d) => case d of inl(_) => 2 | inr(_) => 0⌝ 
   THEN (Reduce 0 THENW Auto)
   THEN RepeatFor 2 (Intro)
   THEN (GenConclTerm ⌜f x y⌝⋅ THENA Auto)
   THEN ((D -2 THEN Reduce 0) THENL [Auto; (D -2 THEN Reduce 0 THEN Auto)])
   THEN D 6
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  \mBbbN{}\msupplus{}
2.  3  *  K  \mmember{}  (r1)/K  <  (r(2))/K
3.  \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))))
\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:
(RenameVar  `f'  (-1)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}x,y.  case  f  x  y  of  inl($_{}$)  =>  1  |  inr(d)  =>  case  d  of  inl(\mbackslash{}f\000Cf24_{}$)  =>  2  |  inr($_{}$)  =>  0\mkleeneclose{} 
  THEN  (Reduce  0  THENW  Auto)
  THEN  RepeatFor  2  (Intro)
  THEN  (GenConclTerm  \mkleeneopen{}f  x  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((D  -2  THEN  Reduce  0)  THENL  [Auto;  (D  -2  THEN  Reduce  0  THEN  Auto)])
  THEN  D  6
  THEN  Unhide
  THEN  Auto)

---

Home Index