---

Step * of Lemma reals-close-or-rneq

No Annotations
∀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
{ (Auto THEN (InstLemma `int-rdiv-rless-witness2` [⌜K⌝]⋅ THENA Auto)) }

1
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))))))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}K:\mBbbN{}\msupplus{}
    (\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:
(Auto  THEN  (InstLemma  `int-rdiv-rless-witness2`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index