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