---

Step * of Lemma nearby-cases

∀n:ℕ+. ∀x,y:ℝ.  ((x < y) ∨ (y < x) ∨ (|x - y| ≤ (r1/r(n))))
BY
{ (Auto
   THEN (Evaluate ⌜m = (4 * n) ∈ ℕ+⌝⋅ THENA Auto)
   THEN (Evaluate ⌜a = (x m) ∈ ℤ⌝⋅ THENA Auto)
   THEN (Evaluate ⌜b = (y m) ∈ ℤ⌝⋅ THENA Auto)) }

1
1. n : ℕ+
2. x : ℝ
3. y : ℝ
4. m : ℕ+
5. m = (4 * n) ∈ ℕ+
6. a : ℤ
7. a = (x m) ∈ ℤ
8. b : ℤ
9. b = (y m) ∈ ℤ
⊢ (x < y) ∨ (y < x) ∨ (|x - y| ≤ (r1/r(n)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbR{}.    ((x  <  y)  \mvee{}  (y  <  x)  \mvee{}  (|x  -  y|  \mleq{}  (r1/r(n))))


By

---

Latex:
(Auto
  THEN  (Evaluate  \mkleeneopen{}m  =  (4  *  n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}a  =  (x  m)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}b  =  (y  m)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index