---

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


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
BY
{ ((ThinVar `a' THEN (RWO "rabs-difference-symmetry" 5 THENA Auto))
   THEN (RWO "rabs-of-nonneg" 5 THENA Auto)
   THEN RWO "5<" (-1)
   THEN Auto
   THEN RWO "rabs-difference-bound-iff" (-1)
   THEN Auto) }

---

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{}
6.  |y  -  a|  =  d
7.  |y  -  b|  =  d
8.  a  <  y
9.  y  <  b
10.  |y  -  x|  <  d
11.  a  <  x
\mvdash{}  x  <  b


By

---

Latex:
((ThinVar  `a'  THEN  (RWO  "rabs-difference-symmetry"  5  THENA  Auto))
  THEN  (RWO  "rabs-of-nonneg"  5  THENA  Auto)
  THEN  RWO  "5<"  (-1)
  THEN  Auto
  THEN  RWO  "rabs-difference-bound-iff"  (-1)
  THEN  Auto)

---

Home Index