---

Step * 1 1 1 of Lemma rationals-dense


1. x : ℝ@i
2. y : {y:ℝ| x < y} @i
3. n : ℕ+
4. (x n) + 4 < y n
5. ((r(y n))/2 * n - (r1/r(n))) ≤ y
6. x ≤ ((r(x n))/2 * n + (r1/r(n)))
⊢ x < (r((x n) + (y n))/r(4 * n))
BY
{ ((RWO "-1" 0 THENA Auto) THEN nRMul ⌜r(4 * n)⌝ 0⋅ THEN (RWO "int-rdiv-req" 0 THENA Auto) THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \{y:\mBbbR{}|  x  <  y\}  @i
3.  n  :  \mBbbN{}\msupplus{}
4.  (x  n)  +  4  <  y  n
5.  ((r(y  n))/2  *  n  -  (r1/r(n)))  \mleq{}  y
6.  x  \mleq{}  ((r(x  n))/2  *  n  +  (r1/r(n)))
\mvdash{}  x  <  (r((x  n)  +  (y  n))/r(4  *  n))


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)
  THEN  nRMul  \mkleeneopen{}r(4  *  n)\mkleeneclose{}  0\mcdot{}
  THEN  (RWO  "int-rdiv-req"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index