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


1. v : ℝ
2. lim n→∞.v * (r(2)/r(3))^n = r0
⊢ lim n→∞.(2^n * v)/3^n = r0
BY
{ TACTIC:(MoveToConcl (-1) THEN BLemma `converges-to_functionality`  THEN Auto) }

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


Latex:


Latex:

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


By


Latex:
TACTIC:(MoveToConcl  (-1)  THEN  BLemma  `converges-to\_functionality`    THEN  Auto)




Home Index