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

Proof

Step	Hyp	Ref	Expression
1		3cn	⊢ 3 ∈ ℂ
2		ax-1cn	⊢ 1 ∈ ℂ
3		picn	⊢ π ∈ ℂ
4		3ne0	⊢ 3 ≠ 0
5	3 1 4	divcli	⊢ ( π / 3 ) ∈ ℂ
6	1 2 5	subdiri	⊢ ( ( 3 − 1 ) · ( π / 3 ) ) = ( ( 3 · ( π / 3 ) ) − ( 1 · ( π / 3 ) ) )
7		3m1e2	⊢ ( 3 − 1 ) = 2
8	7	oveq1i	⊢ ( ( 3 − 1 ) · ( π / 3 ) ) = ( 2 · ( π / 3 ) )
9	3 1 4	divcan2i	⊢ ( 3 · ( π / 3 ) ) = π
10	5	mullidi	⊢ ( 1 · ( π / 3 ) ) = ( π / 3 )
11	9 10	oveq12i	⊢ ( ( 3 · ( π / 3 ) ) − ( 1 · ( π / 3 ) ) ) = ( π − ( π / 3 ) )
12	6 8 11	3eqtr3i	⊢ ( 2 · ( π / 3 ) ) = ( π − ( π / 3 ) )
13	12	fveq2i	⊢ ( cos ‘ ( 2 · ( π / 3 ) ) ) = ( cos ‘ ( π − ( π / 3 ) ) )
14		cospim	⊢ ( ( π / 3 ) ∈ ℂ → ( cos ‘ ( π − ( π / 3 ) ) ) = - ( cos ‘ ( π / 3 ) ) )
15	5 14	ax-mp	⊢ ( cos ‘ ( π − ( π / 3 ) ) ) = - ( cos ‘ ( π / 3 ) )
16		sincos3rdpi	⊢ ( ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) )
17	16	simpri	⊢ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 )
18	17	negeqi	⊢ - ( cos ‘ ( π / 3 ) ) = - ( 1 / 2 )
19	13 15 18	3eqtri	⊢ ( cos ‘ ( 2 · ( π / 3 ) ) ) = - ( 1 / 2 )