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 · ( π / 3 ) ) ) = - ( 1 / 2 )

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		3cn	⊢ 3 ∈ ℂ
3		3ne0	⊢ 3 ≠ 0
4	1 2 3	divcli	⊢ ( π / 3 ) ∈ ℂ
5		cosppi	⊢ ( ( π / 3 ) ∈ ℂ → ( cos ‘ ( ( π / 3 ) + π ) ) = - ( cos ‘ ( π / 3 ) ) )
6	4 5	ax-mp	⊢ ( cos ‘ ( ( π / 3 ) + π ) ) = - ( cos ‘ ( π / 3 ) )
7		3rdpwhole	⊢ ( π ∈ ℂ → ( ( π / 3 ) + π ) = ( 4 · ( π / 3 ) ) )
8	1 7	ax-mp	⊢ ( ( π / 3 ) + π ) = ( 4 · ( π / 3 ) )
9	8	fveq2i	⊢ ( cos ‘ ( ( π / 3 ) + π ) ) = ( cos ‘ ( 4 · ( π / 3 ) ) )
10		sincos3rdpi	⊢ ( ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) )
11	10	simpri	⊢ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 )
12	11	negeqi	⊢ - ( cos ‘ ( π / 3 ) ) = - ( 1 / 2 )
13	6 9 12	3eqtr3i	⊢ ( cos ‘ ( 4 · ( π / 3 ) ) ) = - ( 1 / 2 )