---

Step * of Lemma rationals-dense

No Annotations
∀x:ℝ. ∀y:{y:ℝ| x < y} .  ∃n:ℕ+. ∃m:ℤ. ((x < (r(m)/r(n))) ∧ ((r(m)/r(n)) < y))
BY
{ (TACTIC:Auto
   THEN (Evaluate ⌜n = rlessw(x;y) ∈ {n:ℕ+| (x n) + 4 < y n} ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (Assert (x n) + 4 < y n BY
               (Unhide THEN Auto))⋅
   THEN Thin (-2)
   THEN (InstConcl [⌜4 * n⌝;⌜(x n) + (y n)⌝]⋅ THENA Auto)) }

1
1. x : ℝ@i
2. y : {y:ℝ| x < y} @i
3. n : ℕ+
4. (x n) + 4 < y n
⊢ (x < (r((x n) + (y n))/r(4 * n))) ∧ ((r((x n) + (y n))/r(4 * n)) < y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  <  y\}  .    \mexists{}n:\mBbbN{}\msupplus{}.  \mexists{}m:\mBbbZ{}.  ((x  <  (r(m)/r(n)))  \mwedge{}  ((r(m)/r(n))  <  y))


By

---

Latex:
(TACTIC:Auto
  THEN  (Evaluate  \mkleeneopen{}n  =  rlessw(x;y)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (Assert  (x  n)  +  4  <  y  n  BY
                          (Unhide  THEN  Auto))\mcdot{}
  THEN  Thin  (-2)
  THEN  (InstConcl  [\mkleeneopen{}4  *  n\mkleeneclose{};\mkleeneopen{}(x  n)  +  (y  n)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index