---

Step * 1 1 1 2 1 2 1 1 of Lemma cantor-to-interval-req


1. v : ℝ
2. n : ℕ
3. ¬(3^n = 0 ∈ ℤ)
4. r(3)^n ≠ r0
⊢ (v * (r(2^n)/r(3^n))) = (2^n * v)/3^n
BY
{ ((RWO  "int-rdiv-req" 0 THENA Auto) THEN (RWO  "int-rmul-req" 0 THENA Auto)) }

1
1. v : ℝ
2. n : ℕ
3. ¬(3^n = 0 ∈ ℤ)
4. r(3)^n ≠ r0
⊢ (v * (r(2^n)/r(3^n))) = (r(2^n) * v/r(3^n))

---

Latex:

---

Latex:

1.  v  :  \mBbbR{}
2.  n  :  \mBbbN{}
3.  \mneg{}(3\^{}n  =  0)
4.  r(3)\^{}n  \mneq{}  r0
\mvdash{}  (v  *  (r(2\^{}n)/r(3\^{}n)))  =  (2\^{}n  *  v)/3\^{}n


By

---

Latex:
((RWO    "int-rdiv-req"  0  THENA  Auto)  THEN  (RWO    "int-rmul-req"  0  THENA  Auto))

---

Home Index