---

Step * 1 1 1 1 1 1 1 of Lemma dyadic-rationals-dense


1. a : {a:ℝ| a ∈ (-∞, ∞)} 
2. b : {r:ℝ| r ∈ (-∞, ∞)} 
3. x : ℝ
4. y : ℝ
5. d : ℝ
⊢ ((|y - a| = d) ∧ (|y - b| = d)) ⇒ ((a < y) ∧ (y < b)) ⇒ (|y - x| < d) ⇒ ((a < x) ∧ (x < b))
BY
{ Auto }

1
1. a : {a:ℝ| a ∈ (-∞, ∞)} 
2. b : {r:ℝ| r ∈ (-∞, ∞)} 
3. x : ℝ
4. y : ℝ
5. d : ℝ
6. |y - a| = d
7. |y - b| = d
8. a < y
9. y < b
10. |y - x| < d
⊢ a < x

2
1. a : {a:ℝ| a ∈ (-∞, ∞)} 
2. b : {r:ℝ| r ∈ (-∞, ∞)} 
3. x : ℝ
4. y : ℝ
5. d : ℝ
6. |y - a| = d
7. |y - b| = d
8. a < y
9. y < b
10. |y - x| < d
11. a < x
⊢ x < b

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  a  \mmember{}  (-\minfty{},  \minfty{})\} 
2.  b  :  \{r:\mBbbR{}|  r  \mmember{}  (-\minfty{},  \minfty{})\} 
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
5.  d  :  \mBbbR{}
\mvdash{}  ((|y  -  a|  =  d)  \mwedge{}  (|y  -  b|  =  d))  {}\mRightarrow{}  ((a  <  y)  \mwedge{}  (y  <  b))  {}\mRightarrow{}  (|y  -  x|  <  d)  {}\mRightarrow{}  ((a  <  x)  \mwedge{}  (x  <  b))


By

---

Latex:
Auto

---

Home Index