Theorem cos2pi

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

	Ref	Expression
Assertion	cos2pi	⊢ ( cos ‘ ( 2 · π ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		cos2t	⊢ ( π ∈ ℂ → ( cos ‘ ( 2 · π ) ) = ( ( 2 · ( ( cos ‘ π ) ↑ 2 ) ) − 1 ) )
3	1 2	ax-mp	⊢ ( cos ‘ ( 2 · π ) ) = ( ( 2 · ( ( cos ‘ π ) ↑ 2 ) ) − 1 )
4		cospi	⊢ ( cos ‘ π ) = - 1
5	4	oveq1i	⊢ ( ( cos ‘ π ) ↑ 2 ) = ( - 1 ↑ 2 )
6		ax-1cn	⊢ 1 ∈ ℂ
7		sqneg	⊢ ( 1 ∈ ℂ → ( - 1 ↑ 2 ) = ( 1 ↑ 2 ) )
8	6 7	ax-mp	⊢ ( - 1 ↑ 2 ) = ( 1 ↑ 2 )
9		sq1	⊢ ( 1 ↑ 2 ) = 1
10	5 8 9	3eqtri	⊢ ( ( cos ‘ π ) ↑ 2 ) = 1
11	10	oveq2i	⊢ ( 2 · ( ( cos ‘ π ) ↑ 2 ) ) = ( 2 · 1 )
12		2t1e2	⊢ ( 2 · 1 ) = 2
13	11 12	eqtri	⊢ ( 2 · ( ( cos ‘ π ) ↑ 2 ) ) = 2
14	13	oveq1i	⊢ ( ( 2 · ( ( cos ‘ π ) ↑ 2 ) ) − 1 ) = ( 2 − 1 )
15		2m1e1	⊢ ( 2 − 1 ) = 1
16	3 14 15	3eqtri	⊢ ( cos ‘ ( 2 · π ) ) = 1