---

Step * of Lemma rcos-seq-converges-ext

rcos-seq(n)↓ as n→∞
BY
{ Extract of Obid: rcos-seq-converges
  not unfolding  divide rcos-seq exp-ratio
  finishing with Auto
  normalizes to:
  
  <λn.eval m = 4 * n in
      (rcos-seq(exp-ratio(1;3164556962025316455;0;m;1000000000) + 1) m) ÷ 4
  , λk.((exp-ratio(1;3164556962025316455;0;4 * k;1000000000) + 1) + 1)
  > }

---

Latex:

---

Latex:
rcos-seq(n)\mdownarrow{}  as  n\mrightarrow{}\minfty{}


By

---

Latex:
Extract  of  Obid:  rcos-seq-converges
not  unfolding    divide  rcos-seq  exp-ratio
finishing  with  Auto
normalizes  to:

<\mlambda{}n.eval  m  =  4  *  n  in
        (rcos-seq(exp-ratio(1;3164556962025316455;0;m;1000000000)  +  1)  m)  \mdiv{}  4
,  \mlambda{}k.((exp-ratio(1;3164556962025316455;0;4  *  k;1000000000)  +  1)  +  1)
>

---

Home Index