---

Step * 1 of Lemma avoid-reals-simple


1. L : ℝ List
2. a : ℝ
3. b : ℝ
4. a < b
5. a' : ℝ
6. b' : ℝ
7. a ≤ a'
8. b' ≤ b
9. a' < b'
10. (∀x∈L.(x < a') ∨ (b' < x))
11. a ≤ a'
12. a' < b
⊢ (∀x∈L.a' ≠ x)
BY
{ (RepeatFor 2 (ParallelOp -3) THEN Unfold `rneq` 0 THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  \mBbbR{}  List
2.  a  :  \mBbbR{}
3.  b  :  \mBbbR{}
4.  a  <  b
5.  a'  :  \mBbbR{}
6.  b'  :  \mBbbR{}
7.  a  \mleq{}  a'
8.  b'  \mleq{}  b
9.  a'  <  b'
10.  (\mforall{}x\mmember{}L.(x  <  a')  \mvee{}  (b'  <  x))
11.  a  \mleq{}  a'
12.  a'  <  b
\mvdash{}  (\mforall{}x\mmember{}L.a'  \mneq{}  x)


By

---

Latex:
(RepeatFor  2  (ParallelOp  -3)  THEN  Unfold  `rneq`  0  THEN  D  -1  THEN  Auto)

---

Home Index