Metamath Proof Explorer

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 
|- ( ( sin ` ( _pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( _pi / 6 ) ) = ( ( sqrt ` 3 ) / 2 ) )

Proof

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