---

Step * of Lemma cosine-approx-lemma

∀a:{2...}. ∀N:ℕ+.  (∃k:ℕ [(N ≤ (a^((2 * k) + 2) * ((2 * k) + 2)!))])
BY
{ (Auto
   THEN (Evaluate ⌜aa = (a * a) ∈ {4...}⌝⋅
         THENA (Auto THEN (D 1 THENA Auto) THEN MemTypeCD THEN Auto THEN Mul ⌜a⌝ 2⋅ THEN Auto)
         )
   THEN (RWO "exp2<" (-1) THENA Auto)) }

1
1. a : {2...}
2. N : ℕ+
3. aa : {4...}
4. aa = a^2 ∈ {4...}
⊢ ∃k:ℕ [(N ≤ (a^((2 * k) + 2) * ((2 * k) + 2)!))]

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Evaluate  \mkleeneopen{}aa  =  (a  *  a)\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  (D  1  THENA  Auto)  THEN  MemTypeCD  THEN  Auto  THEN  Mul  \mkleeneopen{}a\mkleeneclose{}  2\mcdot{}  THEN  Auto)
              )
  THEN  (RWO  "exp2<"  (-1)  THENA  Auto))

---

Home Index