---

Step * 4 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)
⊢ ∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ ((x < a') ∨ (b' < x)))
BY
{ ((InstLemma `rless-cases` [⌜(2 * a + b)/3⌝;⌜(a + 2 * b)/3⌝;⌜x⌝]⋅ THENA Auto) THEN D -1) }

1
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)))

2
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. x < (a + 2 * b)/3
⊢ ∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ ((x < a') ∨ (b' < x)))

---

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)
\mvdash{}  \mexists{}a',b':\mBbbR{}.  ((a  \mleq{}  a')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  (a'  <  b')  \mwedge{}  ((x  <  a')  \mvee{}  (b'  <  x)))


By

---

Latex:
((InstLemma  `rless-cases`  [\mkleeneopen{}(2  *  a  +  b)/3\mkleeneclose{};\mkleeneopen{}(a  +  2  *  b)/3\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index