---

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


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(Assert  r(3)\^{}n  \mneq{}  r0  BY
                            (RWO    "rnexp-int"  0  THEN  Auto))

---

Home Index