Theorem sincos6thpi

Description: The sine and cosine of _pi / 6 . (Contributed by Paul Chapman, 25-Jan-2008) (Revised by Wolf Lammen, 24-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		pire	$$⊢\mathrm{\pi }\in ℝ$$
3		6re	$$⊢6\in ℝ$$
4		6pos	$$⊢0<6$$
5	3 4	gt0ne0ii	$$⊢6\ne 0$$
6	2 3 5	redivcli	$$⊢\frac{\mathrm{\pi }}{6}\in ℝ$$
7	6	recni	$$⊢\frac{\mathrm{\pi }}{6}\in ℂ$$
8		sincl	$$⊢\frac{\mathrm{\pi }}{6}\in ℂ\to \sin \left(\frac{\mathrm{\pi }}{6}\right)\in ℂ$$
9	7 8	ax-mp	$$⊢\sin \left(\frac{\mathrm{\pi }}{6}\right)\in ℂ$$
10		2ne0	$$⊢2\ne 0$$
11		recoscl	$$⊢\frac{\mathrm{\pi }}{6}\in ℝ\to \cos \left(\frac{\mathrm{\pi }}{6}\right)\in ℝ$$
12	6 11	ax-mp	$$⊢\cos \left(\frac{\mathrm{\pi }}{6}\right)\in ℝ$$
13	12	recni	$$⊢\cos \left(\frac{\mathrm{\pi }}{6}\right)\in ℂ$$
14	1 9 13	mulassi	$$⊢2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)=2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
15		sin2t	$$⊢\frac{\mathrm{\pi }}{6}\in ℂ\to \sin 2\left(\frac{\mathrm{\pi }}{6}\right)=2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
16	7 15	ax-mp	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{6}\right)=2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
17	14 16	eqtr4i	$$⊢2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)=\sin 2\left(\frac{\mathrm{\pi }}{6}\right)$$
18		3cn	$$⊢3\in ℂ$$
19		3ne0	$$⊢3\ne 0$$
20	1 18 19	divcli	$$⊢\frac{2}{3}\in ℂ$$
21	18 19	reccli	$$⊢\frac{1}{3}\in ℂ$$
22		df-3	$$⊢3=2+1$$
23	22	oveq1i	$$⊢\frac{3}{3}=\frac{2+1}{3}$$
24	18 19	dividi	$$⊢\frac{3}{3}=1$$
25		ax-1cn	$$⊢1\in ℂ$$
26	1 25 18 19	divdiri	$$⊢\frac{2+1}{3}=\left(\frac{2}{3}\right)+\left(\frac{1}{3}\right)$$
27	23 24 26	3eqtr3ri	$$⊢\left(\frac{2}{3}\right)+\left(\frac{1}{3}\right)=1$$
28		sincosq1eq	$$⊢\left(\frac{2}{3}\in ℂ\wedge \frac{1}{3}\in ℂ\wedge \left(\frac{2}{3}\right)+\left(\frac{1}{3}\right)=1\right)\to \sin \left(\frac{2}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\cos \left(\frac{1}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)$$
29	20 21 27 28	mp3an	$$⊢\sin \left(\frac{2}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\cos \left(\frac{1}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)$$
30		picn	$$⊢\mathrm{\pi }\in ℂ$$
31	1 18 30 1 19 10	divmuldivi	$$⊢\left(\frac{2}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\frac{2\mathrm{\pi }}{3\cdot 2}$$
32		3t2e6	$$⊢3\cdot 2=6$$
33	32	oveq2i	$$⊢\frac{2\mathrm{\pi }}{3\cdot 2}=\frac{2\mathrm{\pi }}{6}$$
34		6cn	$$⊢6\in ℂ$$
35	1 30 34 5	divassi	$$⊢\frac{2\mathrm{\pi }}{6}=2\left(\frac{\mathrm{\pi }}{6}\right)$$
36	31 33 35	3eqtri	$$⊢\left(\frac{2}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=2\left(\frac{\mathrm{\pi }}{6}\right)$$
37	36	fveq2i	$$⊢\sin \left(\frac{2}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\sin 2\left(\frac{\mathrm{\pi }}{6}\right)$$
38	29 37	eqtr3i	$$⊢\cos \left(\frac{1}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\sin 2\left(\frac{\mathrm{\pi }}{6}\right)$$
39	25 18 30 1 19 10	divmuldivi	$$⊢\left(\frac{1}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\frac{1\mathrm{\pi }}{3\cdot 2}$$
40	30	mullidi	$$⊢1\mathrm{\pi }=\mathrm{\pi }$$
41	40 32	oveq12i	$$⊢\frac{1\mathrm{\pi }}{3\cdot 2}=\frac{\mathrm{\pi }}{6}$$
42	39 41	eqtri	$$⊢\left(\frac{1}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{6}$$
43	42	fveq2i	$$⊢\cos \left(\frac{1}{3}\right)\left(\frac{\mathrm{\pi }}{2}\right)=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
44	38 43	eqtr3i	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{6}\right)=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
45	17 44	eqtri	$$⊢2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
46	13	mullidi	$$⊢1\cos \left(\frac{\mathrm{\pi }}{6}\right)=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
47	45 46	eqtr4i	$$⊢2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)=1\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
48	1 9	mulcli	$$⊢2\sin \left(\frac{\mathrm{\pi }}{6}\right)\in ℂ$$
49		pipos	$$⊢0<\mathrm{\pi }$$
50	2 3 49 4	divgt0ii	$$⊢0<\frac{\mathrm{\pi }}{6}$$
51		2lt6	$$⊢2<6$$
52		2re	$$⊢2\in ℝ$$
53		2pos	$$⊢0<2$$
54	52 53	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
55	3 4	pm3.2i	$$⊢\left(6\in ℝ\wedge 0<6\right)$$
56	2 49	pm3.2i	$$⊢\left(\mathrm{\pi }\in ℝ\wedge 0<\mathrm{\pi }\right)$$
57		ltdiv2	$$⊢\left(\left(2\in ℝ\wedge 0<2\right)\wedge \left(6\in ℝ\wedge 0<6\right)\wedge \left(\mathrm{\pi }\in ℝ\wedge 0<\mathrm{\pi }\right)\right)\to \left(2<6\leftrightarrow \frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}\right)$$
58	54 55 56 57	mp3an	$$⊢2<6\leftrightarrow \frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}$$
59	51 58	mpbi	$$⊢\frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}$$
60		0re	$$⊢0\in ℝ$$
61		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
62		rexr	$$⊢0\in ℝ\to 0\in {ℝ}^{*}$$
63		rexr	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$$
64		elioo2	$$⊢\left(0\in {ℝ}^{*}\wedge \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\right)\to \left(\frac{\mathrm{\pi }}{6}\in \left(0,\frac{\mathrm{\pi }}{2}\right)\leftrightarrow \left(\frac{\mathrm{\pi }}{6}\in ℝ\wedge 0<\frac{\mathrm{\pi }}{6}\wedge \frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}\right)\right)$$
65	62 63 64	syl2an	$$⊢\left(0\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\right)\to \left(\frac{\mathrm{\pi }}{6}\in \left(0,\frac{\mathrm{\pi }}{2}\right)\leftrightarrow \left(\frac{\mathrm{\pi }}{6}\in ℝ\wedge 0<\frac{\mathrm{\pi }}{6}\wedge \frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}\right)\right)$$
66	60 61 65	mp2an	$$⊢\frac{\mathrm{\pi }}{6}\in \left(0,\frac{\mathrm{\pi }}{2}\right)\leftrightarrow \left(\frac{\mathrm{\pi }}{6}\in ℝ\wedge 0<\frac{\mathrm{\pi }}{6}\wedge \frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}\right)$$
67	6 50 59 66	mpbir3an	$$⊢\frac{\mathrm{\pi }}{6}\in \left(0,\frac{\mathrm{\pi }}{2}\right)$$
68		sincosq1sgn	$$⊢\frac{\mathrm{\pi }}{6}\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(0<\sin \left(\frac{\mathrm{\pi }}{6}\right)\wedge 0<\cos \left(\frac{\mathrm{\pi }}{6}\right)\right)$$
69	67 68	ax-mp	$$⊢\left(0<\sin \left(\frac{\mathrm{\pi }}{6}\right)\wedge 0<\cos \left(\frac{\mathrm{\pi }}{6}\right)\right)$$
70	69	simpri	$$⊢0<\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
71	12 70	gt0ne0ii	$$⊢\cos \left(\frac{\mathrm{\pi }}{6}\right)\ne 0$$
72	13 71	pm3.2i	$$⊢\left(\cos \left(\frac{\mathrm{\pi }}{6}\right)\in ℂ\wedge \cos \left(\frac{\mathrm{\pi }}{6}\right)\ne 0\right)$$
73		mulcan2	$$⊢\left(2\sin \left(\frac{\mathrm{\pi }}{6}\right)\in ℂ\wedge 1\in ℂ\wedge \left(\cos \left(\frac{\mathrm{\pi }}{6}\right)\in ℂ\wedge \cos \left(\frac{\mathrm{\pi }}{6}\right)\ne 0\right)\right)\to \left(2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)=1\cos \left(\frac{\mathrm{\pi }}{6}\right)\leftrightarrow 2\sin \left(\frac{\mathrm{\pi }}{6}\right)=1\right)$$
74	48 25 72 73	mp3an	$$⊢2\sin \left(\frac{\mathrm{\pi }}{6}\right)\cos \left(\frac{\mathrm{\pi }}{6}\right)=1\cos \left(\frac{\mathrm{\pi }}{6}\right)\leftrightarrow 2\sin \left(\frac{\mathrm{\pi }}{6}\right)=1$$
75	47 74	mpbi	$$⊢2\sin \left(\frac{\mathrm{\pi }}{6}\right)=1$$
76	1 9 10 75	mvllmuli	$$⊢\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}$$
77		3re	$$⊢3\in ℝ$$
78		3pos	$$⊢0<3$$
79	77 78	sqrtpclii	$$⊢\sqrt{3}\in ℝ$$
80	79	recni	$$⊢\sqrt{3}\in ℂ$$
81	80 1 10	sqdivi	$$⊢{\left(\frac{\sqrt{3}}{2}\right)}^2=\frac{{\sqrt{3}}^2}{2^2}$$
82	60 77 78	ltleii	$$⊢0\le 3$$
83	77	sqsqrti	$$⊢0\le 3\to {\sqrt{3}}^2=3$$
84	82 83	ax-mp	$$⊢{\sqrt{3}}^2=3$$
85		sq2	$$⊢2^2=4$$
86	84 85	oveq12i	$$⊢\frac{{\sqrt{3}}^2}{2^2}=\frac{3}{4}$$
87	81 86	eqtri	$$⊢{\left(\frac{\sqrt{3}}{2}\right)}^2=\frac{3}{4}$$
88	87	fveq2i	$$⊢\sqrt{{\left(\frac{\sqrt{3}}{2}\right)}^2}=\sqrt{\frac{3}{4}}$$
89	77	sqrtge0i	$$⊢0\le 3\to 0\le \sqrt{3}$$
90	82 89	ax-mp	$$⊢0\le \sqrt{3}$$
91	79 52	divge0i	$$⊢\left(0\le \sqrt{3}\wedge 0<2\right)\to 0\le \frac{\sqrt{3}}{2}$$
92	90 53 91	mp2an	$$⊢0\le \frac{\sqrt{3}}{2}$$
93	79 52 10	redivcli	$$⊢\frac{\sqrt{3}}{2}\in ℝ$$
94	93	sqrtsqi	$$⊢0\le \frac{\sqrt{3}}{2}\to \sqrt{{\left(\frac{\sqrt{3}}{2}\right)}^2}=\frac{\sqrt{3}}{2}$$
95	92 94	ax-mp	$$⊢\sqrt{{\left(\frac{\sqrt{3}}{2}\right)}^2}=\frac{\sqrt{3}}{2}$$
96		4cn	$$⊢4\in ℂ$$
97		4ne0	$$⊢4\ne 0$$
98	96 97	dividi	$$⊢\frac{4}{4}=1$$
99	98	oveq1i	$$⊢\left(\frac{4}{4}\right)-\left(\frac{1}{4}\right)=1-\left(\frac{1}{4}\right)$$
100	96 97	pm3.2i	$$⊢\left(4\in ℂ\wedge 4\ne 0\right)$$
101		divsubdir	$$⊢\left(4\in ℂ\wedge 1\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{4-1}{4}=\left(\frac{4}{4}\right)-\left(\frac{1}{4}\right)$$
102	96 25 100 101	mp3an	$$⊢\frac{4-1}{4}=\left(\frac{4}{4}\right)-\left(\frac{1}{4}\right)$$
103		4m1e3	$$⊢4-1=3$$
104	103	oveq1i	$$⊢\frac{4-1}{4}=\frac{3}{4}$$
105	102 104	eqtr3i	$$⊢\left(\frac{4}{4}\right)-\left(\frac{1}{4}\right)=\frac{3}{4}$$
106	96 97	reccli	$$⊢\frac{1}{4}\in ℂ$$
107	13	sqcli	$$⊢{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2\in ℂ$$
108	76	oveq1i	$$⊢{\sin \left(\frac{\mathrm{\pi }}{6}\right)}^2={\left(\frac{1}{2}\right)}^2$$
109	1 10	sqrecii	$$⊢{\left(\frac{1}{2}\right)}^2=\frac{1}{2^2}$$
110	85	oveq2i	$$⊢\frac{1}{2^2}=\frac{1}{4}$$
111	108 109 110	3eqtri	$$⊢{\sin \left(\frac{\mathrm{\pi }}{6}\right)}^2=\frac{1}{4}$$
112	111	oveq1i	$$⊢{\sin \left(\frac{\mathrm{\pi }}{6}\right)}^2+{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2=\left(\frac{1}{4}\right)+{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2$$
113		sincossq	$$⊢\frac{\mathrm{\pi }}{6}\in ℂ\to {\sin \left(\frac{\mathrm{\pi }}{6}\right)}^2+{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2=1$$
114	7 113	ax-mp	$$⊢{\sin \left(\frac{\mathrm{\pi }}{6}\right)}^2+{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2=1$$
115	112 114	eqtr3i	$$⊢\left(\frac{1}{4}\right)+{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2=1$$
116	25 106 107 115	subaddrii	$$⊢1-\left(\frac{1}{4}\right)={\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2$$
117	99 105 116	3eqtr3ri	$$⊢{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2=\frac{3}{4}$$
118	117	fveq2i	$$⊢\sqrt{{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2}=\sqrt{\frac{3}{4}}$$
119	60 12 70	ltleii	$$⊢0\le \cos \left(\frac{\mathrm{\pi }}{6}\right)$$
120	12	sqrtsqi	$$⊢0\le \cos \left(\frac{\mathrm{\pi }}{6}\right)\to \sqrt{{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2}=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
121	119 120	ax-mp	$$⊢\sqrt{{\cos \left(\frac{\mathrm{\pi }}{6}\right)}^2}=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
122	118 121	eqtr3i	$$⊢\sqrt{\frac{3}{4}}=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
123	88 95 122	3eqtr3ri	$$⊢\cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}$$
124	76 123	pm3.2i	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}\right)$$