Theorem recos4p

Description: Separate out the first four terms of the infinite series expansion of the cosine of a real number. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypothesis	efi4p.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\mathrm{i}A}^n}{n!}\right)$$
Assertion	recos4p	$$⊢A\in ℝ\to \cos A=1-\left(\frac{A^2}{2}\right)+\Re \left(\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		efi4p.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\mathrm{i}A}^n}{n!}\right)$$
2		recosval	$$⊢A\in ℝ\to \cos A=\Re \left({\mathrm{e}}^{\mathrm{i}A}\right)$$
3		recn	$$⊢A\in ℝ\to A\in ℂ$$
4	1	efi4p	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\left(1-\left(\frac{A^2}{2}\right)\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$
5	3 4	syl	$$⊢A\in ℝ\to {\mathrm{e}}^{\mathrm{i}A}=\left(1-\left(\frac{A^2}{2}\right)\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$
6	5	fveq2d	$$⊢A\in ℝ\to \Re \left({\mathrm{e}}^{\mathrm{i}A}\right)=\Re \left(\left(1-\left(\frac{A^2}{2}\right)\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)$$
7		1re	$$⊢1\in ℝ$$
8		resqcl	$$⊢A\in ℝ\to A^2\in ℝ$$
9	8	rehalfcld	$$⊢A\in ℝ\to \frac{A^2}{2}\in ℝ$$
10		resubcl	$$⊢\left(1\in ℝ\wedge \frac{A^2}{2}\in ℝ\right)\to 1-\left(\frac{A^2}{2}\right)\in ℝ$$
11	7 9 10	sylancr	$$⊢A\in ℝ\to 1-\left(\frac{A^2}{2}\right)\in ℝ$$
12	11	recnd	$$⊢A\in ℝ\to 1-\left(\frac{A^2}{2}\right)\in ℂ$$
13		ax-icn	$$⊢\mathrm{i}\in ℂ$$
14		3nn0	$$⊢3\in {\mathbb{N}}_0$$
15		reexpcl	$$⊢\left(A\in ℝ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℝ$$
16	14 15	mpan2	$$⊢A\in ℝ\to A^3\in ℝ$$
17		6re	$$⊢6\in ℝ$$
18		6pos	$$⊢0<6$$
19	17 18	gt0ne0ii	$$⊢6\ne 0$$
20		redivcl	$$⊢\left(A^3\in ℝ\wedge 6\in ℝ\wedge 6\ne 0\right)\to \frac{A^3}{6}\in ℝ$$
21	17 19 20	mp3an23	$$⊢A^3\in ℝ\to \frac{A^3}{6}\in ℝ$$
22	16 21	syl	$$⊢A\in ℝ\to \frac{A^3}{6}\in ℝ$$
23		resubcl	$$⊢\left(A\in ℝ\wedge \frac{A^3}{6}\in ℝ\right)\to A-\left(\frac{A^3}{6}\right)\in ℝ$$
24	22 23	mpdan	$$⊢A\in ℝ\to A-\left(\frac{A^3}{6}\right)\in ℝ$$
25	24	recnd	$$⊢A\in ℝ\to A-\left(\frac{A^3}{6}\right)\in ℂ$$
26		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A-\left(\frac{A^3}{6}\right)\in ℂ\right)\to \mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)\in ℂ$$
27	13 25 26	sylancr	$$⊢A\in ℝ\to \mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)\in ℂ$$
28	12 27	addcld	$$⊢A\in ℝ\to 1-\left(\frac{A^2}{2}\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)\in ℂ$$
29		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
30	13 3 29	sylancr	$$⊢A\in ℝ\to \mathrm{i}A\in ℂ$$
31		4nn0	$$⊢4\in {\mathbb{N}}_0$$
32	1	eftlcl	$$⊢\left(\mathrm{i}A\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to \sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\in ℂ$$
33	30 31 32	sylancl	$$⊢A\in ℝ\to \sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\in ℂ$$
34	28 33	readdd	$$⊢A\in ℝ\to \Re \left(\left(1-\left(\frac{A^2}{2}\right)\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)=\Re \left(1-\left(\frac{A^2}{2}\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)\right)+\Re \left(\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)$$
35	11 24	crred	$$⊢A\in ℝ\to \Re \left(1-\left(\frac{A^2}{2}\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)\right)=1-\left(\frac{A^2}{2}\right)$$
36	35	oveq1d	$$⊢A\in ℝ\to \Re \left(1-\left(\frac{A^2}{2}\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)\right)+\Re \left(\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)=1-\left(\frac{A^2}{2}\right)+\Re \left(\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)$$
37	6 34 36	3eqtrd	$$⊢A\in ℝ\to \Re \left({\mathrm{e}}^{\mathrm{i}A}\right)=1-\left(\frac{A^2}{2}\right)+\Re \left(\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)$$
38	2 37	eqtrd	$$⊢A\in ℝ\to \cos A=1-\left(\frac{A^2}{2}\right)+\Re \left(\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right)$$