Metamath Proof Explorer

Theorem cos4t3rdpi

Description: The cosine of 4 x. ( _pi / 3 ) is -u 1 / 2 . (Contributed by SN, 19-Nov-2025)

Ref Expression
Assertion cos4t3rdpi 
|- ( cos ` ( 4 x. ( _pi / 3 ) ) ) = -u ( 1 / 2 )

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 3cn 
 |-  3 e. CC
3 3ne0 
 |-  3 =/= 0
4 1 2 3 divcli 
 |-  ( _pi / 3 ) e. CC
5 cosppi 
 |-  ( ( _pi / 3 ) e. CC -> ( cos ` ( ( _pi / 3 ) + _pi ) ) = -u ( cos ` ( _pi / 3 ) ) )
6 4 5 ax-mp 
 |-  ( cos ` ( ( _pi / 3 ) + _pi ) ) = -u ( cos ` ( _pi / 3 ) )
7 3rdpwhole 
 |-  ( _pi e. CC -> ( ( _pi / 3 ) + _pi ) = ( 4 x. ( _pi / 3 ) ) )
8 1 7 ax-mp 
 |-  ( ( _pi / 3 ) + _pi ) = ( 4 x. ( _pi / 3 ) )
9 8 fveq2i 
 |-  ( cos ` ( ( _pi / 3 ) + _pi ) ) = ( cos ` ( 4 x. ( _pi / 3 ) ) )
10 sincos3rdpi 
 |-  ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )
11 10 simpri 
 |-  ( cos ` ( _pi / 3 ) ) = ( 1 / 2 )
12 11 negeqi 
 |-  -u ( cos ` ( _pi / 3 ) ) = -u ( 1 / 2 )
13 6 9 12 3eqtr3i 
 |-  ( cos ` ( 4 x. ( _pi / 3 ) ) ) = -u ( 1 / 2 )