Metamath Proof Explorer

Theorem cos2t3rdpi

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

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

Proof

Step Hyp Ref Expression
1 3cn 
 |-  3 e. CC
2 ax-1cn 
 |-  1 e. CC
3 picn 
 |-  _pi e. CC
4 3ne0 
 |-  3 =/= 0
5 3 1 4 divcli 
 |-  ( _pi / 3 ) e. CC
6 1 2 5 subdiri 
 |-  ( ( 3 - 1 ) x. ( _pi / 3 ) ) = ( ( 3 x. ( _pi / 3 ) ) - ( 1 x. ( _pi / 3 ) ) )
7 3m1e2 
 |-  ( 3 - 1 ) = 2
8 7 oveq1i 
 |-  ( ( 3 - 1 ) x. ( _pi / 3 ) ) = ( 2 x. ( _pi / 3 ) )
9 3 1 4 divcan2i 
 |-  ( 3 x. ( _pi / 3 ) ) = _pi
10 5 mullidi 
 |-  ( 1 x. ( _pi / 3 ) ) = ( _pi / 3 )
11 9 10 oveq12i 
 |-  ( ( 3 x. ( _pi / 3 ) ) - ( 1 x. ( _pi / 3 ) ) ) = ( _pi - ( _pi / 3 ) )
12 6 8 11 3eqtr3i 
 |-  ( 2 x. ( _pi / 3 ) ) = ( _pi - ( _pi / 3 ) )
13 12 fveq2i 
 |-  ( cos ` ( 2 x. ( _pi / 3 ) ) ) = ( cos ` ( _pi - ( _pi / 3 ) ) )
14 cospim 
 |-  ( ( _pi / 3 ) e. CC -> ( cos ` ( _pi - ( _pi / 3 ) ) ) = -u ( cos ` ( _pi / 3 ) ) )
15 5 14 ax-mp 
 |-  ( cos ` ( _pi - ( _pi / 3 ) ) ) = -u ( cos ` ( _pi / 3 ) )
16 sincos3rdpi 
 |-  ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )
17 16 simpri 
 |-  ( cos ` ( _pi / 3 ) ) = ( 1 / 2 )
18 17 negeqi 
 |-  -u ( cos ` ( _pi / 3 ) ) = -u ( 1 / 2 )
19 13 15 18 3eqtri 
 |-  ( cos ` ( 2 x. ( _pi / 3 ) ) ) = -u ( 1 / 2 )