---

Step * of Lemma sine-approx-lemma-bad

∀a:{2...}. ∀N:ℕ.  (∃k:ℕ [(N ≤ (a^((2 * k) + 3) * ((2 * k) + 3)!))])
BY
{ ((D 0 THENA Auto) THEN InductionOnNat) }

1
.....basecase..... 
1. a : {2...}
⊢ ∃k:ℕ [(0 ≤ (a^((2 * k) + 3) * ((2 * k) + 3)!))]

2
.....upcase..... 
1. a : {2...}
2. N : ℤ
3. [%1] : 0 < N
4. ∃k:ℕ [((N - 1) ≤ (a^((2 * k) + 3) * ((2 * k) + 3)!))]
⊢ ∃k:ℕ [(N ≤ (a^((2 * k) + 3) * ((2 * k) + 3)!))]

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  InductionOnNat)

---

Home Index