Theorem sincos3rdpi

Description: The sine and cosine of _pi / 3 . (Contributed by Mario Carneiro, 21-May-2016)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		2cn	$$⊢2\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4	2 3	reccli	$$⊢\frac{1}{2}\in ℂ$$
5		3cn	$$⊢3\in ℂ$$
6		3ne0	$$⊢3\ne 0$$
7	5 6	reccli	$$⊢\frac{1}{3}\in ℂ$$
8	1 4 7	subdii	$$⊢\mathrm{\pi }\left(\left(\frac{1}{2}\right)-\left(\frac{1}{3}\right)\right)=\mathrm{\pi }\left(\frac{1}{2}\right)-\mathrm{\pi }\left(\frac{1}{3}\right)$$
9		halfthird	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{3}\right)=\frac{1}{6}$$
10	9	oveq2i	$$⊢\mathrm{\pi }\left(\left(\frac{1}{2}\right)-\left(\frac{1}{3}\right)\right)=\mathrm{\pi }\left(\frac{1}{6}\right)$$
11	8 10	eqtr3i	$$⊢\mathrm{\pi }\left(\frac{1}{2}\right)-\mathrm{\pi }\left(\frac{1}{3}\right)=\mathrm{\pi }\left(\frac{1}{6}\right)$$
12	1 2 3	divreci	$$⊢\frac{\mathrm{\pi }}{2}=\mathrm{\pi }\left(\frac{1}{2}\right)$$
13	1 5 6	divreci	$$⊢\frac{\mathrm{\pi }}{3}=\mathrm{\pi }\left(\frac{1}{3}\right)$$
14	12 13	oveq12i	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)=\mathrm{\pi }\left(\frac{1}{2}\right)-\mathrm{\pi }\left(\frac{1}{3}\right)$$
15		6cn	$$⊢6\in ℂ$$
16		6nn	$$⊢6\in \mathbb{N}$$
17	16	nnne0i	$$⊢6\ne 0$$
18	1 15 17	divreci	$$⊢\frac{\mathrm{\pi }}{6}=\mathrm{\pi }\left(\frac{1}{6}\right)$$
19	11 14 18	3eqtr4i	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)=\frac{\mathrm{\pi }}{6}$$
20	19	fveq2i	$$⊢\cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
21	1 5 6	divcli	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ$$
22		coshalfpim	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\sin \left(\frac{\mathrm{\pi }}{3}\right)$$
23	21 22	ax-mp	$$⊢\cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\sin \left(\frac{\mathrm{\pi }}{3}\right)$$
24		sincos6thpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}\right)$$
25	24	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}$$
26	20 23 25	3eqtr3i	$$⊢\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}$$
27	19	fveq2i	$$⊢\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\sin \left(\frac{\mathrm{\pi }}{6}\right)$$
28		sinhalfpim	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
29	21 28	ax-mp	$$⊢\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{3}\right)\right)=\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
30	24	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}$$
31	27 29 30	3eqtr3i	$$⊢\cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}$$
32	26 31	pm3.2i	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}\right)$$