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 ` _pi ) = -u 1

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 2cn 
 |-  2 e. CC
3 2ne0 
 |-  2 =/= 0
4 1 2 3 divcli 
 |-  ( _pi / 2 ) e. CC
5 cos2t 
 |-  ( ( _pi / 2 ) e. CC -> ( cos ` ( 2 x. ( _pi / 2 ) ) ) = ( ( 2 x. ( ( cos ` ( _pi / 2 ) ) ^ 2 ) ) - 1 ) )
6 4 5 ax-mp 
 |-  ( cos ` ( 2 x. ( _pi / 2 ) ) ) = ( ( 2 x. ( ( cos ` ( _pi / 2 ) ) ^ 2 ) ) - 1 )
7 1 2 3 divcan2i 
 |-  ( 2 x. ( _pi / 2 ) ) = _pi
8 7 fveq2i 
 |-  ( cos ` ( 2 x. ( _pi / 2 ) ) ) = ( cos ` _pi )
9 coshalfpi 
 |-  ( cos ` ( _pi / 2 ) ) = 0
10 9 oveq1i 
 |-  ( ( cos ` ( _pi / 2 ) ) ^ 2 ) = ( 0 ^ 2 )
11 sq0 
 |-  ( 0 ^ 2 ) = 0
12 10 11 eqtri 
 |-  ( ( cos ` ( _pi / 2 ) ) ^ 2 ) = 0
13 12 oveq2i 
 |-  ( 2 x. ( ( cos ` ( _pi / 2 ) ) ^ 2 ) ) = ( 2 x. 0 )
14 2t0e0 
 |-  ( 2 x. 0 ) = 0
15 13 14 eqtri 
 |-  ( 2 x. ( ( cos ` ( _pi / 2 ) ) ^ 2 ) ) = 0
16 15 oveq1i 
 |-  ( ( 2 x. ( ( cos ` ( _pi / 2 ) ) ^ 2 ) ) - 1 ) = ( 0 - 1 )
17 df-neg 
 |-  -u 1 = ( 0 - 1 )
18 16 17 eqtr4i 
 |-  ( ( 2 x. ( ( cos ` ( _pi / 2 ) ) ^ 2 ) ) - 1 ) = -u 1
19 6 8 18 3eqtr3i 
 |-  ( cos ` _pi ) = -u 1