This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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