---

Step * 2 1 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. (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ))
16. r(3^n) = (r(3^(n - 1)) * r(3))
⊢ ((r(2) * v1) + v2/r(3)) = ((r(3^n - (2 * v3) + v4) * a) + (r((2 * v3) + v4) * b)/r(3^n))
BY
{ (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 "int-rdiv-req" (-3) THENA Auto)
   THEN (RWO "-4 -3" 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) }

---

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.  (\mneg{}(3\^{}(n  -  1)  =  0))  \mwedge{}  (\mneg{}(3\^{}n  =  0))
16.  r(3\^{}n)  =  (r(3\^{}(n  -  1))  *  r(3))
\mvdash{}  ((r(2)  *  v1)  +  v2/r(3))  =  ((r(3\^{}n  -  (2  *  v3)  +  v4)  *  a)  +  (r((2  *  v3)  +  v4)  *  b)/r(3\^{}n))


By

---

Latex:
(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  "int-rdiv-req"  (-3)  THENA  Auto)
  THEN  (RWO  "-4  -3"  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)

---

Home Index