---

Step * 1 1 1 of Lemma fun-converges-to-cosine


1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
2. m : ℕ+
3. r0 ≤ (r1/r(4))
4. (r1/r(4)) < r1
5. n : {m...}
6. x : {x:ℝ| |x| ≤ r(m)} 
⊢ |(x^2 * (n + 1))/(2 * (n + 1))!| ≤ ((r1/r(4)) * |(x^2 * n)/(2 * n)!|)
BY
{ ((D -2 THENA Auto) THEN (Assert 1 ≤ m BY  Id)) }

1
.....aux..... 
1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
2. m : ℕ+
3. r0 ≤ (r1/r(4))
4. (r1/r(4)) < r1
5. n : ℤ
6. m ≤ n
7. x : {x:ℝ| |x| ≤ r(m)} 
⊢ 1 ≤ m

2
1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
2. m : ℕ+
3. r0 ≤ (r1/r(4))
4. (r1/r(4)) < r1
5. n : ℤ
6. m ≤ n
7. x : {x:ℝ| |x| ≤ r(m)} 
8. 1 ≤ m
⊢ |(x^2 * (n + 1))/(2 * (n + 1))!| ≤ ((r1/r(4)) * |(x^2 * n)/(2 * n)!|)

---

Latex:

---

Latex:

1.  \mforall{}x:\mBbbR{}.  \mSigma{}i.-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  =  cosine(x)
2.  m  :  \mBbbN{}\msupplus{}
3.  r0  \mleq{}  (r1/r(4))
4.  (r1/r(4))  <  r1
5.  n  :  \{m...\}
6.  x  :  \{x:\mBbbR{}|  |x|  \mleq{}  r(m)\} 
\mvdash{}  |(x\^{}2  *  (n  +  1))/(2  *  (n  +  1))!|  \mleq{}  ((r1/r(4))  *  |(x\^{}2  *  n)/(2  *  n)!|)


By

---

Latex:
((D  -2  THENA  Auto)  THEN  (Assert  1  \mleq{}  m  BY    Id))

---

Home Index