---

Step * of Lemma cosine-exists-ext1

∀x:ℝ. {a:ℝ| Σi.-1^i * (x^2 * i)/(2 * i)! = a} 
BY
{ Extract of Obid: cosine-exists
  normalizes to:
  
  λx.eval y = x in
     λn.eval m = 4 * n in
        (Σ{-1^i * (y^2 * i)/(2 * i)! | 0≤i≤imax(imax(if canonical-bound(y)=0
                                                        then expfact(1;canonical-bound(y);m * canonical-bound(y);1)
                                                        else expfact(1;canonical-bound(y);m * canonical-bound(y);1);0);
                                                canonical-bound(y) ÷ 2)} 
         m) ÷ 4
  
  not unfolding  rational-approx canonical-bound rsum rmul rabs rnexp int-rdiv int-rmul rdiv fact fastexp expfact  imax
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \{a:\mBbbR{}|  \mSigma{}i.-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  =  a\} 


By

---

Latex:
...

---

Home Index