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	$⊢ (\sin (\frac{π}{6}) = \frac{1}{2} \land \cos (\frac{π}{6}) = \frac{\sqrt{3}}{2})$

Proof

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

Metamath Proof Explorer

Theorem sincos6thpi

Proof