---

Step * of Lemma cantor-middle-third-lemma

∀x,a,b:ℝ.  ((x ∈ [(2 * a + b)/3, b]) ∨ (x ∈ [a, (a + 2 * b)/3])) supposing ((x ∈ [a, b]) and (a < b))
BY
{ (Auto
   THEN RepUR ``i-member`` -1
   THEN RepUR ``i-member`` 0
   THEN (InstLemma `rless-cases` [⌜(2 * a + b)/3⌝;⌜(a + 2 * b)/3⌝;⌜x⌝]⋅ THENM ParallelLast)
   THEN Auto) }

1
.....antecedent..... 
1. x : ℝ
2. a : ℝ
3. b : ℝ
4. [%] : a < b
5. [%1] : (a ≤ x) ∧ (x ≤ b)
⊢ (2 * a + b)/3 < (a + 2 * b)/3

2
1. x : ℝ
2. a : ℝ
3. b : ℝ
4. [%] : a < b
5. [%1] : (a ≤ x) ∧ (x ≤ b)
6. (2 * a + b)/3 < x
7. (2 * a + b)/3 ≤ x
⊢ x ≤ b

3
1. x : ℝ
2. a : ℝ
3. b : ℝ
4. [%] : a < b
5. [%1] : (a ≤ x) ∧ (x ≤ b)
6. x < (a + 2 * b)/3
⊢ a ≤ x

---

Latex:

---

Latex:
\mforall{}x,a,b:\mBbbR{}.
    ((x  \mmember{}  [(2  *  a  +  b)/3,  b])  \mvee{}  (x  \mmember{}  [a,  (a  +  2  *  b)/3]))  supposing  ((x  \mmember{}  [a,  b])  and  (a  <  b))


By

---

Latex:
(Auto
  THEN  RepUR  ``i-member``  -1
  THEN  RepUR  ``i-member``  0
  THEN  (InstLemma  `rless-cases`  [\mkleeneopen{}(2  *  a  +  b)/3\mkleeneclose{};\mkleeneopen{}(a  +  2  *  b)/3\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  ParallelLast)
  THEN  Auto)

---

Home Index