Theorem cospi

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

	Ref	Expression
Assertion	cospi	⊢ ( cos ‘ π ) = - 1

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		2cn	⊢ 2 ∈ ℂ
3		2ne0	⊢ 2 ≠ 0
4	1 2 3	divcli	⊢ ( π / 2 ) ∈ ℂ
5		cos2t	⊢ ( ( π / 2 ) ∈ ℂ → ( cos ‘ ( 2 · ( π / 2 ) ) ) = ( ( 2 · ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) ) − 1 ) )
6	4 5	ax-mp	⊢ ( cos ‘ ( 2 · ( π / 2 ) ) ) = ( ( 2 · ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) ) − 1 )
7	1 2 3	divcan2i	⊢ ( 2 · ( π / 2 ) ) = π
8	7	fveq2i	⊢ ( cos ‘ ( 2 · ( π / 2 ) ) ) = ( cos ‘ π )
9		coshalfpi	⊢ ( cos ‘ ( π / 2 ) ) = 0
10	9	oveq1i	⊢ ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) = ( 0 ↑ 2 )
11		sq0	⊢ ( 0 ↑ 2 ) = 0
12	10 11	eqtri	⊢ ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) = 0
13	12	oveq2i	⊢ ( 2 · ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) ) = ( 2 · 0 )
14		2t0e0	⊢ ( 2 · 0 ) = 0
15	13 14	eqtri	⊢ ( 2 · ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) ) = 0
16	15	oveq1i	⊢ ( ( 2 · ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) ) − 1 ) = ( 0 − 1 )
17		df-neg	⊢ - 1 = ( 0 − 1 )
18	16 17	eqtr4i	⊢ ( ( 2 · ( ( cos ‘ ( π / 2 ) ) ↑ 2 ) ) − 1 ) = - 1
19	6 8 18	3eqtr3i	⊢ ( cos ‘ π ) = - 1