Theorem sin2t3rdpi

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

	Ref	Expression
Assertion	sin2t3rdpi	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{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	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{3}\right)=\sin \left(\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)\right)$$
14		sinpim	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \sin \left(\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\sin \left(\frac{\mathrm{\pi }}{3}\right)$$
15	5 14	ax-mp	$$⊢\sin \left(\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\sin \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	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}$$
18	13 15 17	3eqtri	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}$$