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

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		3cn	$$⊢3\in ℂ$$
3		3ne0	$$⊢3\ne 0$$
4	1 2 3	divcli	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ$$
5		cosppi	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }\right)=-\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
6	4 5	ax-mp	$$⊢\cos \left(\left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }\right)=-\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
7		3rdpwhole	$$⊢\mathrm{\pi }\in ℂ\to \left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }=4\left(\frac{\mathrm{\pi }}{3}\right)$$
8	1 7	ax-mp	$$⊢\left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }=4\left(\frac{\mathrm{\pi }}{3}\right)$$
9	8	fveq2i	$$⊢\cos \left(\left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }\right)=\cos 4\left(\frac{\mathrm{\pi }}{3}\right)$$
10		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)$$
11	10	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}$$
12	11	negeqi	$$⊢-\cos \left(\frac{\mathrm{\pi }}{3}\right)=-\frac{1}{2}$$
13	6 9 12	3eqtr3i	$$⊢\cos 4\left(\frac{\mathrm{\pi }}{3}\right)=-\frac{1}{2}$$