---

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


1. v : ℝ
2. n : ℕ
⊢ (v * (r(2)/r(3))^n) = (2^n * v)/3^n
BY
{ TACTIC:Assert ⌜¬(3^n = 0 ∈ ℤ)⌝⋅ }

1
.....assertion..... 
1. v : ℝ
2. n : ℕ
⊢ ¬(3^n = 0 ∈ ℤ)

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

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mneg{}(3\^{}n  =  0)\mkleeneclose{}\mcdot{}

---

Home Index