---

Step * of Lemma cantor-common-middle-third-lemma

∀x,y,a,b:ℝ.
  (((x ∈ [(2 * a + b)/3, b]) ∧ (y ∈ [(2 * a + b)/3, b]))
     ∨ ((x ∈ [a, (a + 2 * b)/3]) ∧ (y ∈ [a, (a + 2 * b)/3]))) supposing 
     (((x ∈ [a, b]) ∧ (y ∈ [a, b]) ∧ (|x - y| ≤ (b - a/r(6)))) and 
     (a < b))
BY
{ (Auto
   THEN (Assert a < b BY
               Auto)
   THEN (Assert (a + b)/2 < (a + 2 * b)/3 BY
               ((RWO "int-rdiv-req" 0 THENA Auto)
                THEN (RWO "int-rmul-req" 0 THENA Auto)
                THEN nRMul ⌜r(2) * r(3)⌝ 0⋅
                THEN Auto
                THEN RWO  "rmul-int" 0
                THEN Auto))
   THEN (Assert (2 * a + b)/3 < (a + b)/2 BY
               ((RWO "int-rdiv-req" 0 THENA Auto)
                THEN (RWO "int-rmul-req" 0 THENA Auto)
                THEN nRMul ⌜r(2) * r(3)⌝ 0⋅
                THEN Auto
                THEN RWO  "rmul-int" 0
                THEN Auto))) }

1
1. x : ℝ
2. y : ℝ
3. a : ℝ
4. b : ℝ
5. [%] : a < b
6. [%1] : (x ∈ [a, b]) ∧ (y ∈ [a, b]) ∧ (|x - y| ≤ (b - a/r(6)))
7. a < b
8. (a + b)/2 < (a + 2 * b)/3
9. (2 * a + b)/3 < (a + b)/2
⊢ ((x ∈ [(2 * a + b)/3, b]) ∧ (y ∈ [(2 * a + b)/3, b])) ∨ ((x ∈ [a, (a + 2 * b)/3]) ∧ (y ∈ [a, (a + 2 * b)/3]))

---

Latex:

---

Latex:
\mforall{}x,y,a,b:\mBbbR{}.
    (((x  \mmember{}  [(2  *  a  +  b)/3,  b])  \mwedge{}  (y  \mmember{}  [(2  *  a  +  b)/3,  b]))
          \mvee{}  ((x  \mmember{}  [a,  (a  +  2  *  b)/3])  \mwedge{}  (y  \mmember{}  [a,  (a  +  2  *  b)/3])))  supposing 
          (((x  \mmember{}  [a,  b])  \mwedge{}  (y  \mmember{}  [a,  b])  \mwedge{}  (|x  -  y|  \mleq{}  (b  -  a/r(6))))  and 
          (a  <  b))


By

---

Latex:
(Auto
  THEN  (Assert  a  <  b  BY
                          Auto)
  THEN  (Assert  (a  +  b)/2  <  (a  +  2  *  b)/3  BY
                          ((RWO  "int-rdiv-req"  0  THENA  Auto)
                            THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
                            THEN  nRMul  \mkleeneopen{}r(2)  *  r(3)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto
                            THEN  RWO    "rmul-int"  0
                            THEN  Auto))
  THEN  (Assert  (2  *  a  +  b)/3  <  (a  +  b)/2  BY
                          ((RWO  "int-rdiv-req"  0  THENA  Auto)
                            THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
                            THEN  nRMul  \mkleeneopen{}r(2)  *  r(3)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto
                            THEN  RWO    "rmul-int"  0
                            THEN  Auto)))

---

Home Index