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 ‘ ( π / 6 ) ) = ( 1 / 2 ) ∧ ( cos ‘ ( π / 6 ) ) = ( ( √ ‘ 3 ) / 2 ) )

Proof

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