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

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 picn 
 |-  _pi e. CC
3 1 2 mulcli 
 |-  ( 2 x. _pi ) e. CC
4 3 mulm1i 
 |-  ( -u 1 x. ( 2 x. _pi ) ) = -u ( 2 x. _pi )
5 4 oveq2i 
 |-  ( _pi + ( -u 1 x. ( 2 x. _pi ) ) ) = ( _pi + -u ( 2 x. _pi ) )
6 2 3 negsubi 
 |-  ( _pi + -u ( 2 x. _pi ) ) = ( _pi - ( 2 x. _pi ) )
7 sub2times 
 |-  ( _pi e. CC -> ( _pi - ( 2 x. _pi ) ) = -u _pi )
8 2 7 ax-mp 
 |-  ( _pi - ( 2 x. _pi ) ) = -u _pi
9 5 6 8 3eqtrri 
 |-  -u _pi = ( _pi + ( -u 1 x. ( 2 x. _pi ) ) )
10 9 fveq2i 
 |-  ( cos ` -u _pi ) = ( cos ` ( _pi + ( -u 1 x. ( 2 x. _pi ) ) ) )
11 neg1z 
 |-  -u 1 e. ZZ
12 cosper 
 |-  ( ( _pi e. CC /\ -u 1 e. ZZ ) -> ( cos ` ( _pi + ( -u 1 x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
13 2 11 12 mp2an 
 |-  ( cos ` ( _pi + ( -u 1 x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi )
14 cospi 
 |-  ( cos ` _pi ) = -u 1
15 10 13 14 3eqtri 
 |-  ( cos ` -u _pi ) = -u 1