---

Step * 2 3 of Lemma cantor-interval-req


1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
5. ¬↑(f (n - 1))
6. 0 < n
7. v1 : ℝ
8. v2 : ℝ
9. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
10. v3 : ℤ
11. v4 : ℤ
12. unit-interval-fan(f;n - 1) = <v3, v4> ∈ (ℤ × ℤ)
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))
⊢ v1 = ((r(3^n - 3 * v3) * a) + (r(3 * v3) * 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 "-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) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
4.  n  :  \mBbbZ{}
5.  \mneg{}\muparrow{}(f  (n  -  1))
6.  0  <  n
7.  v1  :  \mBbbR{}
8.  v2  :  \mBbbR{}
9.  cantor-interval(a;b;f;n  -  1)  =  <v1,  v2>
10.  v3  :  \mBbbZ{}
11.  v4  :  \mBbbZ{}
12.  unit-interval-fan(f;n  -  1)  =  <v3,  v4>
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{}  v1  =  ((r(3\^{}n  -  3  *  v3)  *  a)  +  (r(3  *  v3)  *  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  "-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)

---

Home Index