---

Step * 1 of Lemma avoid-reals


1. u : ℝ
2. v : ℝ List
3. ∀a,b:ℝ.  ((a < b) ⇒ (∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ (∀x∈v.(x < a') ∨ (b' < x)))))
4. a : ℝ
5. b : ℝ
6. a < b
7. a' : ℝ
8. b' : ℝ
9. a ≤ a'
10. b' ≤ b
11. a' < b'
12. (∀x∈v.(x < a') ∨ (b' < x))
13. a'@0 : ℝ
14. b'@0 : ℝ
15. a' ≤ a'@0
16. b'@0 ≤ b'
17. a'@0 < b'@0
18. (u < a'@0) ∨ (b'@0 < u)
19. a ≤ a'@0
20. b'@0 ≤ b
21. a'@0 < b'@0
22. (u < a'@0) ∨ (b'@0 < u)
⊢ (∀x∈v.(x < a'@0) ∨ (b'@0 < x))
BY
{ RepeatFor 2 (ParallelOp 12) }

1
1. u : ℝ
2. v : ℝ List
3. ∀a,b:ℝ.  ((a < b) ⇒ (∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ (∀x∈v.(x < a') ∨ (b' < x)))))
4. a : ℝ
5. b : ℝ
6. a < b
7. a' : ℝ
8. b' : ℝ
9. a ≤ a'
10. b' ≤ b
11. a' < b'
12. ∀i:ℕ||v||. ((v[i] < a') ∨ (b' < v[i]))
13. a'@0 : ℝ
14. b'@0 : ℝ
15. a' ≤ a'@0
16. b'@0 ≤ b'
17. a'@0 < b'@0
18. (u < a'@0) ∨ (b'@0 < u)
19. a ≤ a'@0
20. b'@0 ≤ b
21. a'@0 < b'@0
22. (u < a'@0) ∨ (b'@0 < u)
23. i : ℕ||v||
24. (v[i] < a') ∨ (b' < v[i])
⊢ (v[i] < a'@0) ∨ (b'@0 < v[i])

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  \mforall{}a,b:\mBbbR{}.    ((a  <  b)  {}\mRightarrow{}  (\mexists{}a',b':\mBbbR{}.  ((a  \mleq{}  a')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  (a'  <  b')  \mwedge{}  (\mforall{}x\mmember{}v.(x  <  a')  \mvee{}  (b'  <  x)))))
4.  a  :  \mBbbR{}
5.  b  :  \mBbbR{}
6.  a  <  b
7.  a'  :  \mBbbR{}
8.  b'  :  \mBbbR{}
9.  a  \mleq{}  a'
10.  b'  \mleq{}  b
11.  a'  <  b'
12.  (\mforall{}x\mmember{}v.(x  <  a')  \mvee{}  (b'  <  x))
13.  a'@0  :  \mBbbR{}
14.  b'@0  :  \mBbbR{}
15.  a'  \mleq{}  a'@0
16.  b'@0  \mleq{}  b'
17.  a'@0  <  b'@0
18.  (u  <  a'@0)  \mvee{}  (b'@0  <  u)
19.  a  \mleq{}  a'@0
20.  b'@0  \mleq{}  b
21.  a'@0  <  b'@0
22.  (u  <  a'@0)  \mvee{}  (b'@0  <  u)
\mvdash{}  (\mforall{}x\mmember{}v.(x  <  a'@0)  \mvee{}  (b'@0  <  x))


By

---

Latex:
RepeatFor  2  (ParallelOp  12)

---

Home Index