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

Metamath Proof Explorer

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