---

Step * 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))) ∧ ((r((x n) + (y n))/r(4 * n)) < y)
BY
{ D 0 }

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

2
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)))
⊢ (r((x n) + (y n))/r(4 * n)) < y

---

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)))  \mwedge{}  ((r((x  n)  +  (y  n))/r(4  *  n))  <  y)


By

---

Latex:
D  0

---

Home Index