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\left(\frac{\mathrm{\pi }}{3}\right)=-\frac{1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		3cn	$$⊢3\in ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		picn	$$⊢\mathrm{\pi }\in ℂ$$
4		3ne0	$$⊢3\ne 0$$
5	3 1 4	divcli	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ$$
6	1 2 5	subdiri	$$⊢\left(3-1\right)\left(\frac{\mathrm{\pi }}{3}\right)=3\left(\frac{\mathrm{\pi }}{3}\right)-1\left(\frac{\mathrm{\pi }}{3}\right)$$
7		3m1e2	$$⊢3-1=2$$
8	7	oveq1i	$$⊢\left(3-1\right)\left(\frac{\mathrm{\pi }}{3}\right)=2\left(\frac{\mathrm{\pi }}{3}\right)$$
9	3 1 4	divcan2i	$$⊢3\left(\frac{\mathrm{\pi }}{3}\right)=\mathrm{\pi }$$
10	5	mullidi	$$⊢1\left(\frac{\mathrm{\pi }}{3}\right)=\frac{\mathrm{\pi }}{3}$$
11	9 10	oveq12i	$$⊢3\left(\frac{\mathrm{\pi }}{3}\right)-1\left(\frac{\mathrm{\pi }}{3}\right)=\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)$$
12	6 8 11	3eqtr3i	$$⊢2\left(\frac{\mathrm{\pi }}{3}\right)=\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)$$
13	12	fveq2i	$$⊢\cos 2\left(\frac{\mathrm{\pi }}{3}\right)=\cos \left(\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)\right)$$
14		cospim	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \cos \left(\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)\right)=-\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
15	5 14	ax-mp	$$⊢\cos \left(\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)\right)=-\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
16		sincos3rdpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}\right)$$
17	16	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}$$
18	17	negeqi	$$⊢-\cos \left(\frac{\mathrm{\pi }}{3}\right)=-\frac{1}{2}$$
19	13 15 18	3eqtri	$$⊢\cos 2\left(\frac{\mathrm{\pi }}{3}\right)=-\frac{1}{2}$$