---

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


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

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "rnexp-rdiv<"  0  THENA  Auto)  THEN  RWO    "rnexp-int"  0  THEN  Auto)

---

Home Index