---

Step * 4 1 of Lemma avoid-real


1. a : ℝ
2. b : ℝ
3. x : ℝ
4. a < b
5. (a < (2 * a + b)/3) ∧ ((2 * a + b)/3 < (a + 2 * b)/3) ∧ ((a + 2 * b)/3 < b)
6. (2 * a + b)/3 < x
⊢ ∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ ((x < a') ∨ (b' < x)))
BY
{ (InstConcl [⌜a⌝;⌜(2 * a + b)/3⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  x  :  \mBbbR{}
4.  a  <  b
5.  (a  <  (2  *  a  +  b)/3)  \mwedge{}  ((2  *  a  +  b)/3  <  (a  +  2  *  b)/3)  \mwedge{}  ((a  +  2  *  b)/3  <  b)
6.  (2  *  a  +  b)/3  <  x
\mvdash{}  \mexists{}a',b':\mBbbR{}.  ((a  \mleq{}  a')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  (a'  <  b')  \mwedge{}  ((x  <  a')  \mvee{}  (b'  <  x)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}(2  *  a  +  b)/3\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index