---

Step * 2 4 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. v1 = (3^n - 3 * v3 * a + 3 * v3 * b)/3^n
16. (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ))
17. r(3^n) = (r(3^(n - 1)) * r(3))
⊢ (v1 + (r(2) * v2)/r(3)) = ((r(3^n - v3 + (2 * v4)) * a) + (r(v3 + (2 * v4)) * b)/r(3^n))
BY
{ Thin (-3) }

1
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(2) * v2)/r(3)) = ((r(3^n - v3 + (2 * v4)) * a) + (r(v3 + (2 * v4)) * b)/r(3^n))

---

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


By

---

Latex:
Thin  (-3)

---

Home Index