---

Step * of Lemma sine-approx-lemma-bad-ext

∀a:{2...}. ∀N:ℕ.  (∃k:ℕ [(N ≤ (a^((2 * k) + 3) * ((2 * k) + 3)!))])
BY
{ Extract of Obid: sine-approx-lemma-bad
  not unfolding  primrec exp fact recdefs
  finishing with Auto
  normalizes to:
  
  λa,N. primrec(N;0;λi,x. if (a^((2 * x) + 3) * ((2 * x) + 3)!) < (i + 1)  then x + 1  else x) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  sine-approx-lemma-bad
not  unfolding    primrec  exp  fact  recdefs
finishing  with  Auto
normalizes  to:

\mlambda{}a,N.  primrec(N;0;\mlambda{}i,x.  if  (a\^{}((2  *  x)  +  3)  *  ((2  *  x)  +  3)!)  <  (i  +  1)    then  x  +  1    else  x)

---

Home Index