Theorem cosnegpi

Description: The cosine of negative _pi is negative 1 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2		picn	⊢ π ∈ ℂ
3	1 2	mulcli	⊢ ( 2 · π ) ∈ ℂ
4	3	mulm1i	⊢ ( - 1 · ( 2 · π ) ) = - ( 2 · π )
5	4	oveq2i	⊢ ( π + ( - 1 · ( 2 · π ) ) ) = ( π + - ( 2 · π ) )
6	2 3	negsubi	⊢ ( π + - ( 2 · π ) ) = ( π − ( 2 · π ) )
7		sub2times	⊢ ( π ∈ ℂ → ( π − ( 2 · π ) ) = - π )
8	2 7	ax-mp	⊢ ( π − ( 2 · π ) ) = - π
9	5 6 8	3eqtrri	⊢ - π = ( π + ( - 1 · ( 2 · π ) ) )
10	9	fveq2i	⊢ ( cos ‘ - π ) = ( cos ‘ ( π + ( - 1 · ( 2 · π ) ) ) )
11		neg1z	⊢ - 1 ∈ ℤ
12		cosper	⊢ ( ( π ∈ ℂ ∧ - 1 ∈ ℤ ) → ( cos ‘ ( π + ( - 1 · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
13	2 11 12	mp2an	⊢ ( cos ‘ ( π + ( - 1 · ( 2 · π ) ) ) ) = ( cos ‘ π )
14		cospi	⊢ ( cos ‘ π ) = - 1
15	10 13 14	3eqtri	⊢ ( cos ‘ - π ) = - 1