---

Step * of Lemma cosine-approx-lemma-ext

∀a:{2...}. ∀N:ℕ+.  (∃k:ℕ [(N ≤ (a^((2 * k) + 2) * ((2 * k) + 2)!))])
BY
{ Extract of Obid: cosine-approx-lemma
  not unfolding  genfact-inv
  finishing with Auto
  normalizes to:
  
  λa,N. eval aa = a * a in genfact-inv(N;2 * aa;k.aa * ((2 * k) + 2) * ((2 * k) + 1)) }

---

Latex:

---

Latex:
\mforall{}a:\{2...\}.  \mforall{}N:\mBbbN{}\msupplus{}.    (\mexists{}k:\mBbbN{}  [(N  \mleq{}  (a\^{}((2  *  k)  +  2)  *  ((2  *  k)  +  2)!))])


By

---

Latex:
Extract  of  Obid:  cosine-approx-lemma
not  unfolding    genfact-inv
finishing  with  Auto
normalizes  to:

\mlambda{}a,N.  eval  aa  =  a  *  a  in  genfact-inv(N;2  *  aa;k.aa  *  ((2  *  k)  +  2)  *  ((2  *  k)  +  1))

---

Home Index