Theorem sincos6thpi 8711

Description: The sine and cosine of pi / 6. (Contributed by Paul Chapman, 25-Jan-2008.)

Assertion

Ref	Expression
sincos6thpi	|- ((sin` (pi / 6)) = (1 / 2) /\ (cos` (pi / 6)) = ((sqr` 3) / 2))

Proof of Theorem sincos6thpi

Step	Hyp	Ref	Expression
1		2cn 5980	. . . . . . . 8 |- 2 e. CC
2		pire 8677	. . . . . . . . . . 11 |- pi e. RR
3		6re 5984	. . . . . . . . . . 11 |- 6 e. RR
4		6pos 5994	. . . . . . . . . . . 12 |- 0 < 6
5	3, 4	gt0ne0i 5617	. . . . . . . . . . 11 |- 6 =/= 0
6	2, 3, 5	redivcl 5798	. . . . . . . . . 10 |- (pi / 6) e. RR
7	6	recn 5314	. . . . . . . . 9 |- (pi / 6) e. CC
8		sinclt 7431	. . . . . . . . 9 |- ((pi / 6) e. CC -> (sin` (pi / 6)) e. CC)
9	7, 8	ax-mp 7	. . . . . . . 8 |- (sin` (pi / 6)) e. CC
10		recosclt 7439	. . . . . . . . . 10 |- ((pi / 6) e. RR -> (cos` (pi / 6)) e. RR)
11	6, 10	ax-mp 7	. . . . . . . . 9 |- (cos` (pi / 6)) e. RR
12	11	recn 5314	. . . . . . . 8 |- (cos` (pi / 6)) e. CC
13	1, 9, 12	mulass 5325	. . . . . . 7 |- ((2 x. (sin` (pi / 6))) x. (cos` (pi / 6))) = (2 x. ((sin` (pi / 6)) x. (cos` (pi / 6))))
14		sin2tt 7462	. . . . . . . 8 |- ((pi / 6) e. CC -> (sin` (2 x. (pi / 6))) = (2 x. ((sin` (pi / 6)) x. (cos` (pi / 6)))))
15	7, 14	ax-mp 7	. . . . . . 7 |- (sin` (2 x. (pi / 6))) = (2 x. ((sin` (pi / 6)) x. (cos` (pi / 6))))
16		3re 5981	. . . . . . . . . . 11 |- 3 e. RR
17	16	recn 5314	. . . . . . . . . 10 |- 3 e. CC
18		3pos 5991	. . . . . . . . . . 11 |- 0 < 3
19	16, 18	gt0ne0i 5617	. . . . . . . . . 10 |- 3 =/= 0
20	1, 17, 19	divcl 5710	. . . . . . . . 9 |- (2 / 3) e. CC
21	17, 19	reccl 5713	. . . . . . . . 9 |- (1 / 3) e. CC
22		df-3 5971	. . . . . . . . . . 11 |- 3 = (2 + 1)
23	22	opreq1i 3971	. . . . . . . . . 10 |- (3 / 3) = ((2 + 1) / 3)
24	17, 19	divid 5770	. . . . . . . . . 10 |- (3 / 3) = 1
25		ax1cn 5269	. . . . . . . . . . 11 |- 1 e. CC
26	1, 25, 17, 19	divdir 5747	. . . . . . . . . 10 |- ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
27	23, 24, 26	3eqtr3r 1504	. . . . . . . . 9 |- ((2 / 3) + (1 / 3)) = 1
28		sincosq1eq 8709	. . . . . . . . 9 |- (((2 / 3) e. CC /\ (1 / 3) e. CC /\ ((2 / 3) + (1 / 3)) = 1) -> (sin` ((2 / 3) x. (pi / 2))) = (cos` ((1 / 3) x. (pi / 2))))
29	20, 21, 27, 28	mp3an 916	. . . . . . . 8 |- (sin` ((2 / 3) x. (pi / 2))) = (cos` ((1 / 3) x. (pi / 2)))
30	2	recn 5314	. . . . . . . . . . 11 |- pi e. CC
31		2ne0 5990	. . . . . . . . . . 11 |- 2 =/= 0
32	1, 17, 30, 1, 19, 31	divmuldiv 5786	. . . . . . . . . 10 |- ((2 / 3) x. (pi / 2)) = ((2 x. pi) / (3 x. 2))
33		3t2e6 6023	. . . . . . . . . . 11 |- (3 x. 2) = 6
34	33	opreq2i 3972	. . . . . . . . . 10 |- ((2 x. pi) / (3 x. 2)) = ((2 x. pi) / 6)
35	3	recn 5314	. . . . . . . . . . 11 |- 6 e. CC
36	1, 30, 35, 5	divass 5746	. . . . . . . . . 10 |- ((2 x. pi) / 6) = (2 x. (pi / 6))
37	32, 34, 36	3eqtr 1499	. . . . . . . . 9 |- ((2 / 3) x. (pi / 2)) = (2 x. (pi / 6))
38	37	fveq2i 3727	. . . . . . . 8 |- (sin` ((2 / 3) x. (pi / 2))) = (sin` (2 x. (pi / 6)))
39	25, 17, 30, 1, 19, 31	divmuldiv 5786	. . . . . . . . . 10 |- ((1 / 3) x. (pi / 2)) = ((1 x. pi) / (3 x. 2))
40	30	mulid2 5333	. . . . . . . . . . 11 |- (1 x. pi) = pi
41	40, 33	opreq12i 3973	. . . . . . . . . 10 |- ((1 x. pi) / (3 x. 2)) = (pi / 6)
42	39, 41	eqtr 1495	. . . . . . . . 9 |- ((1 / 3) x. (pi / 2)) = (pi / 6)
43	42	fveq2i 3727	. . . . . . . 8 |- (cos` ((1 / 3) x. (pi / 2))) = (cos` (pi / 6))
44	29, 38, 43	3eqtr3 1503	. . . . . . 7 |- (sin` (2 x. (pi / 6))) = (cos` (pi / 6))
45	13, 15, 44	3eqtr2 1501	. . . . . 6 |- ((2 x. (sin` (pi / 6))) x. (cos` (pi / 6))) = (cos` (pi / 6))
46	12	mulid2 5333	. . . . . 6 |- (1 x. (cos` (pi / 6))) = (cos` (pi / 6))
47	45, 46	eqtr4 1498	. . . . 5 |- ((2 x. (sin` (pi / 6))) x. (cos` (pi / 6))) = (1 x. (cos` (pi / 6)))
48	1, 9	mulcl 5321	. . . . . 6 |- (2 x. (sin` (pi / 6))) e. CC
49		pipos 8678	. . . . . . . . . . . 12 |- 0 < pi
50	2, 3, 49, 4	divgt0i 5860	. . . . . . . . . . 11 |- 0 < (pi / 6)
51	25	addid2 5331	. . . . . . . . . . . . . . . 16 |- (0 + 1) = 1
52		2pos 5989	. . . . . . . . . . . . . . . . 17 |- 0 < 2
53		0re 5440	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
54		2re 5979	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR
55		1re 5435	. . . . . . . . . . . . . . . . . 18 |- 1 e. RR
56	53, 54, 55	ltadd1 5591	. . . . . . . . . . . . . . . . 17 |- (0 < 2 <-> (0 + 1) < (2 + 1))
57	52, 56	mpbi 189	. . . . . . . . . . . . . . . 16 |- (0 + 1) < (2 + 1)
58	51, 57	eqbrtrr 2636	. . . . . . . . . . . . . . 15 |- 1 < (2 + 1)
59	58, 22	breqtrr 2640	. . . . . . . . . . . . . 14 |- 1 < 3
60	55, 16, 54, 52	ltmul1i 5821	. . . . . . . . . . . . . 14 |- (1 < 3 <-> (1 x. 2) < (3 x. 2))
61	59, 60	mpbi 189	. . . . . . . . . . . . 13 |- (1 x. 2) < (3 x. 2)
62	1	mulid2 5333	. . . . . . . . . . . . 13 |- (1 x. 2) = 2
63	61, 62, 33	3brtr3 2642	. . . . . . . . . . . 12 |- 2 < 6
64	54, 3, 2	3pm3.2i 818	. . . . . . . . . . . . . 14 |- (2 e. RR /\ 6 e. RR /\ pi e. RR)
65		ltdiv2t 5887	. . . . . . . . . . . . . 14 |- (((2 e. RR /\ 6 e. RR /\ pi e. RR) /\ (0 < 2 /\ 0 < 6 /\ 0 < pi)) -> (2 < 6 <-> (pi / 6) < (pi / 2)))
66	64, 65	mpan 695	. . . . . . . . . . . . 13 |- ((0 < 2 /\ 0 < 6 /\ 0 < pi) -> (2 < 6 <-> (pi / 6) < (pi / 2)))
67	52, 4, 49, 66	mp3an 916	. . . . . . . . . . . 12 |- (2 < 6 <-> (pi / 6) < (pi / 2))
68	63, 67	mpbi 189	. . . . . . . . . . 11 |- (pi / 6) < (pi / 2)
69	2, 54, 31	redivcl 5798	. . . . . . . . . . . . 13 |- (pi / 2) e. RR
70		elioo2t 6379	. . . . . . . . . . . . . 14 |- ((0 e. RR* /\ (pi / 2) e. RR*) -> ((pi / 6) e. (0(,)(pi / 2)) <-> ((pi / 6) e. RR /\ 0 < (pi / 6) /\ (pi / 6) < (pi / 2))))
71		rexrt 5499	. . . . . . . . . . . . . 14 |- (0 e. RR -> 0 e. RR*)
72		rexrt 5499	. . . . . . . . . . . . . 14 |- ((pi / 2) e. RR -> (pi / 2) e. RR*)
73	70, 71, 72	syl2an 454	. . . . . . . . . . . . 13 |- ((0 e. RR /\ (pi / 2) e. RR) -> ((pi / 6) e. (0(,)(pi / 2)) <-> ((pi / 6) e. RR /\ 0 < (pi / 6) /\ (pi / 6) < (pi / 2))))
74	53, 69, 73	mp2an 697	. . . . . . . . . . . 12 |- ((pi / 6) e. (0(,)(pi / 2)) <-> ((pi / 6) e. RR /\ 0 < (pi / 6) /\ (pi / 6) < (pi / 2)))
75	74	biimpr 152	. . . . . . . . . . 11 |- (((pi / 6) e. RR /\ 0 < (pi / 6) /\ (pi / 6) < (pi / 2)) -> (pi / 6) e. (0(,)(pi / 2)))
76	6, 50, 68, 75	mp3an 916	. . . . . . . . . 10 |- (pi / 6) e. (0(,)(pi / 2))
77		sincosq1sgn 8704	. . . . . . . . . 10 |- ((pi / 6) e. (0(,)(pi / 2)) -> (0 < (sin` (pi / 6)) /\ 0 < (cos` (pi / 6))))
78	76, 77	ax-mp 7	. . . . . . . . 9 |- (0 < (sin` (pi / 6)) /\ 0 < (cos` (pi / 6)))
79	78	pm3.27i 324	. . . . . . . 8 |- 0 < (cos` (pi / 6))
80	11, 79	gt0ne0i 5617	. . . . . . 7 |- (cos` (pi / 6)) =/= 0
81		mulcan2tOLD 5693	. . . . . . 7 |- ((((2 x. (sin` (pi / 6))) e. CC /\ 1 e. CC /\ (cos` (pi / 6)) e. CC) /\ (cos` (pi / 6)) =/= 0) -> (((2 x. (sin` (pi / 6))) x. (cos` (pi / 6))) = (1 x. (cos` (pi / 6))) <-> (2 x. (sin` (pi / 6))) = 1))
82	80, 81	mpan2 696	. . . . . 6 |- (((2 x. (sin` (pi / 6))) e. CC /\ 1 e. CC /\ (cos` (pi / 6)) e. CC) -> (((2 x. (sin` (pi / 6))) x. (cos` (pi / 6))) = (1 x. (cos` (pi / 6))) <-> (2 x. (sin` (pi / 6))) = 1))
83	48, 25, 12, 82	mp3an 916	. . . . 5 |- (((2 x. (sin` (pi / 6))) x. (cos` (pi / 6))) = (1 x. (cos` (pi / 6))) <-> (2 x. (sin` (pi / 6))) = 1)
84	47, 83	mpbi 189	. . . 4 |- (2 x. (sin` (pi / 6))) = 1
85	25, 1, 9, 31	divmul 5705	. . . 4 |- ((1 / 2) = (sin` (pi / 6)) <-> (2 x. (sin` (pi / 6))) = 1)
86	84, 85	mpbir 190	. . 3 |- (1 / 2) = (sin` (pi / 6))
87	86	eqcomi 1479	. 2 |- (sin` (pi / 6)) = (1 / 2)
88		4re 5982	. . . . . . . 8 |- 4 e. RR
89	88	recn 5314	. . . . . . 7 |- 4 e. CC
90		4pos 5992	. . . . . . . 8 |- 0 < 4
91	88, 90	gt0ne0i 5617	. . . . . . 7 |- 4 =/= 0
92	89, 91	reccl 5713	. . . . . 6 |- (1 / 4) e. CC
93	12	sqc