Theorem cos2pi

Description: The cosine of 2 _pi is 1. (Contributed by Paul Chapman, 23-Jan-2008)

	Ref	Expression
Assertion	cos2pi	$$⊢\cos 2\mathrm{\pi }=1$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		cos2t	$$⊢\mathrm{\pi }\in ℂ\to \cos 2\mathrm{\pi }=2{\cos \mathrm{\pi }}^2-1$$
3	1 2	ax-mp	$$⊢\cos 2\mathrm{\pi }=2{\cos \mathrm{\pi }}^2-1$$
4		cospi	$$⊢\cos \mathrm{\pi }=-1$$
5	4	oveq1i	$$⊢{\cos \mathrm{\pi }}^2={\left(-1\right)}^2$$
6		ax-1cn	$$⊢1\in ℂ$$
7		sqneg	$$⊢1\in ℂ\to {\left(-1\right)}^2=1^2$$
8	6 7	ax-mp	$$⊢{\left(-1\right)}^2=1^2$$
9		sq1	$$⊢1^2=1$$
10	5 8 9	3eqtri	$$⊢{\cos \mathrm{\pi }}^2=1$$
11	10	oveq2i	$$⊢2{\cos \mathrm{\pi }}^2=2\cdot 1$$
12		2t1e2	$$⊢2\cdot 1=2$$
13	11 12	eqtri	$$⊢2{\cos \mathrm{\pi }}^2=2$$
14	13	oveq1i	$$⊢2{\cos \mathrm{\pi }}^2-1=2-1$$
15		2m1e1	$$⊢2-1=1$$
16	3 14 15	3eqtri	$$⊢\cos 2\mathrm{\pi }=1$$