---

Step * 2 2 of Lemma cantor-interval-req


1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
5. 0 < n
6. v1 : ℝ
7. v2 : ℝ
8. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
9. v3 : ℤ
10. v4 : ℤ
11. unit-interval-fan(f;n - 1) = <v3, v4> ∈ (ℤ × ℤ)
12. ↑(f (n - 1))
13. v1 = (3^(n - 1) - v3 * a + v3 * b)/3^(n - 1)
14. v2 = (3^(n - 1) - v4 * a + v4 * b)/3^(n - 1)
15. (2 * v1 + v2)/3 = (3^n - (2 * v3) + v4 * a + (2 * v3) + v4 * b)/3^n
16. (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ))
17. r(3^n) = (r(3^(n - 1)) * r(3))
⊢ v2 = ((r(3^n - 3 * v4) * a) + (r(3 * v4) * b)/r(3^n))
BY
{ xxx(nRMul ⌜r(3^n)⌝ 0⋅
      THEN (RWO  "-1" 0 THENA Auto)
      THEN (nRNorm 0 THENA Auto)
      THEN (RWO "int-rdiv-req" (-4) THENA Auto)
      THEN (RWO "-4" 0 THENA Auto)
      THEN (Assert 0 < 3^(n - 1) BY
                  Auto)
      THEN MoveToConcl (-1)
      THEN (GenConclTerm ⌜3^(n - 1)⌝⋅ THENA Auto)
      THEN (D 0 THENA Auto)
      THEN (RWO "int-rmul-req" 0 THENA Auto)
      THEN nRNorm 0
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  v1  :  \mBbbR{}
7.  v2  :  \mBbbR{}
8.  cantor-interval(a;b;f;n  -  1)  =  <v1,  v2>
9.  v3  :  \mBbbZ{}
10.  v4  :  \mBbbZ{}
11.  unit-interval-fan(f;n  -  1)  =  <v3,  v4>
12.  \muparrow{}(f  (n  -  1))
13.  v1  =  (3\^{}(n  -  1)  -  v3  *  a  +  v3  *  b)/3\^{}(n  -  1)
14.  v2  =  (3\^{}(n  -  1)  -  v4  *  a  +  v4  *  b)/3\^{}(n  -  1)
15.  (2  *  v1  +  v2)/3  =  (3\^{}n  -  (2  *  v3)  +  v4  *  a  +  (2  *  v3)  +  v4  *  b)/3\^{}n
16.  (\mneg{}(3\^{}(n  -  1)  =  0))  \mwedge{}  (\mneg{}(3\^{}n  =  0))
17.  r(3\^{}n)  =  (r(3\^{}(n  -  1))  *  r(3))
\mvdash{}  v2  =  ((r(3\^{}n  -  3  *  v4)  *  a)  +  (r(3  *  v4)  *  b)/r(3\^{}n))


By

---

Latex:
xxx(nRMul  \mkleeneopen{}r(3\^{}n)\mkleeneclose{}  0\mcdot{}
        THEN  (RWO    "-1"  0  THENA  Auto)
        THEN  (nRNorm  0  THENA  Auto)
        THEN  (RWO  "int-rdiv-req"  (-4)  THENA  Auto)
        THEN  (RWO  "-4"  0  THENA  Auto)
        THEN  (Assert  0  <  3\^{}(n  -  1)  BY
                                Auto)
        THEN  MoveToConcl  (-1)
        THEN  (GenConclTerm  \mkleeneopen{}3\^{}(n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  (D  0  THENA  Auto)
        THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
        THEN  nRNorm  0
        THEN  Auto)xxx

---

Home Index