---

Step * 1 of Lemma rationals-dense


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)
BY
{ ((InstLemma `rational-approx-property2` [⌜y⌝;⌜n⌝]⋅ THENA Auto)
   THEN Unfold `rational-approx` (-1)
   THEN (InstLemma `rational-approx-property1` [⌜x⌝;⌜n⌝]⋅ THENA Auto)
   THEN Unfold `rational-approx` (-1))⋅ }

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


By

---

Latex:
((InstLemma  `rational-approx-property2`  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `rational-approx`  (-1)
  THEN  (InstLemma  `rational-approx-property1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `rational-approx`  (-1))\mcdot{}

---

Home Index