Theorem sin4t3rdpi

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

	Ref	Expression
Assertion	sin4t3rdpi	$$⊢\sin 4\left(\frac{\mathrm{\pi }}{3}\right)=-\frac{\sqrt{3}}{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		sinppi	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }\right)=-\sin \left(\frac{\mathrm{\pi }}{3}\right)$$
6	4 5	ax-mp	$$⊢\sin \left(\left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }\right)=-\sin \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	$$⊢\sin \left(\left(\frac{\mathrm{\pi }}{3}\right)+\mathrm{\pi }\right)=\sin 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	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}$$
12	11	negeqi	$$⊢-\sin \left(\frac{\mathrm{\pi }}{3}\right)=-\frac{\sqrt{3}}{2}$$
13	6 9 12	3eqtr3i	$$⊢\sin 4\left(\frac{\mathrm{\pi }}{3}\right)=-\frac{\sqrt{3}}{2}$$