---

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


1. v : ℝ
2. lim n→∞.v = v
3. lim n→∞.(r(2)/r(3))^n = r0
4. lim n→∞.v * (r(2)/r(3))^n = v * r0
⊢ lim n→∞.v * (r(2)/r(3))^n = r0
BY
{ TACTIC:(Assert (v * r0) = r0 BY
                (nRNorm 0 THEN Auto)) }

1
1. v : ℝ
2. lim n→∞.v = v
3. lim n→∞.(r(2)/r(3))^n = r0
4. lim n→∞.v * (r(2)/r(3))^n = v * r0
5. (v * r0) = r0
⊢ lim n→∞.v * (r(2)/r(3))^n = r0

---

Latex:

---

Latex:

1.  v  :  \mBbbR{}
2.  lim  n\mrightarrow{}\minfty{}.v  =  v
3.  lim  n\mrightarrow{}\minfty{}.(r(2)/r(3))\^{}n  =  r0
4.  lim  n\mrightarrow{}\minfty{}.v  *  (r(2)/r(3))\^{}n  =  v  *  r0
\mvdash{}  lim  n\mrightarrow{}\minfty{}.v  *  (r(2)/r(3))\^{}n  =  r0


By

---

Latex:
TACTIC:(Assert  (v  *  r0)  =  r0  BY
                            (nRNorm  0  THEN  Auto))

---

Home Index