---

Step * of Lemma sine-approx-lemma-ext

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

---

Latex:

---

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


By

---

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

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

---

Home Index