Metamath Proof Explorer

Theorem sin2h

Description: Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018)

Ref Expression
Assertion sin2h ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( sin ‘ ( 𝐴 / 2 ) ) = ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 2re ⊢ 2 ∈ ℝ
3 pire ⊢ π ∈ ℝ
4 2 3 remulcli ⊢ ( 2 · π ) ∈ ℝ
5 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ ) → ( 0 [,] ( 2 · π ) ) ⊆ ℝ )
6 1 4 5 mp2an ⊢ ( 0 [,] ( 2 · π ) ) ⊆ ℝ
7 6 sseli ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → 𝐴 ∈ ℝ )
8 7 rehalfcld ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( 𝐴 / 2 ) ∈ ℝ )
9 8 resincld ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
10 1re ⊢ 1 ∈ ℝ
11 recoscl ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
12 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ∈ ℝ ) → ( 1 − ( cos ‘ 𝐴 ) ) ∈ ℝ )
13 10 11 12 sylancr ⊢ ( 𝐴 ∈ ℝ → ( 1 − ( cos ‘ 𝐴 ) ) ∈ ℝ )
14 13 rehalfcld ⊢ ( 𝐴 ∈ ℝ → ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ∈ ℝ )
15 cosbnd ⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) ≤ 1 ) )
16 15 simprd ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ≤ 1 )
17 subge0 ⊢ ( ( 1 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( cos ‘ 𝐴 ) ) ↔ ( cos ‘ 𝐴 ) ≤ 1 ) )
18 10 11 17 sylancr ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ ( 1 − ( cos ‘ 𝐴 ) ) ↔ ( cos ‘ 𝐴 ) ≤ 1 ) )
19 halfnneg2 ⊢ ( ( 1 − ( cos ‘ 𝐴 ) ) ∈ ℝ → ( 0 ≤ ( 1 − ( cos ‘ 𝐴 ) ) ↔ 0 ≤ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )
20 13 19 syl ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ ( 1 − ( cos ‘ 𝐴 ) ) ↔ 0 ≤ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )
21 18 20 bitr3d ⊢ ( 𝐴 ∈ ℝ → ( ( cos ‘ 𝐴 ) ≤ 1 ↔ 0 ≤ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )
22 16 21 mpbid ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) )
23 14 22 resqrtcld ⊢ ( 𝐴 ∈ ℝ → ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) ∈ ℝ )
24 7 23 syl ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) ∈ ℝ )
25 1 4 elicc2i ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · π ) ) )
26 halfnneg2 ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ 0 ≤ ( 𝐴 / 2 ) ) )
27 2pos ⊢ 0 < 2
28 2 27 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
29 ledivmul ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝐴 / 2 ) ≤ π ↔ 𝐴 ≤ ( 2 · π ) ) )
30 3 28 29 mp3an23 ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 / 2 ) ≤ π ↔ 𝐴 ≤ ( 2 · π ) ) )
31 30 bicomd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≤ ( 2 · π ) ↔ ( 𝐴 / 2 ) ≤ π ) )
32 26 31 anbi12d ⊢ ( 𝐴 ∈ ℝ → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · π ) ) ↔ ( 0 ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ π ) ) )
33 rehalfcl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ )
34 33 rexrd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ* )
35 0xr ⊢ 0 ∈ ℝ*
36 3 rexri ⊢ π ∈ ℝ*
37 elicc4 ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ ( 𝐴 / 2 ) ∈ ℝ* ) → ( ( 𝐴 / 2 ) ∈ ( 0 [,] π ) ↔ ( 0 ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ π ) ) )
38 35 36 37 mp3an12 ⊢ ( ( 𝐴 / 2 ) ∈ ℝ* → ( ( 𝐴 / 2 ) ∈ ( 0 [,] π ) ↔ ( 0 ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ π ) ) )
39 34 38 syl ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 / 2 ) ∈ ( 0 [,] π ) ↔ ( 0 ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ π ) ) )
40 32 39 bitr4d ⊢ ( 𝐴 ∈ ℝ → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · π ) ) ↔ ( 𝐴 / 2 ) ∈ ( 0 [,] π ) ) )
41 40 biimpd ⊢ ( 𝐴 ∈ ℝ → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · π ) ) → ( 𝐴 / 2 ) ∈ ( 0 [,] π ) ) )
42 41 3impib ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · π ) ) → ( 𝐴 / 2 ) ∈ ( 0 [,] π ) )
43 25 42 sylbi ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( 𝐴 / 2 ) ∈ ( 0 [,] π ) )
44 sinq12ge0 ⊢ ( ( 𝐴 / 2 ) ∈ ( 0 [,] π ) → 0 ≤ ( sin ‘ ( 𝐴 / 2 ) ) )
45 43 44 syl ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → 0 ≤ ( sin ‘ ( 𝐴 / 2 ) ) )
46 14 22 sqrtge0d ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )
47 7 46 syl ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → 0 ≤ ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )
48 7 recnd ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → 𝐴 ∈ ℂ )
49 ax-1cn ⊢ 1 ∈ ℂ
50 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
51 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ∈ ℂ ) → ( 1 − ( cos ‘ 𝐴 ) ) ∈ ℂ )
52 49 50 51 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( cos ‘ 𝐴 ) ) ∈ ℂ )
53 52 halfcld ⊢ ( 𝐴 ∈ ℂ → ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ∈ ℂ )
54 53 sqsqrtd ⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) ↑ 2 ) = ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) )
55 halfcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 2 ) ∈ ℂ )
56 coscl ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℂ )
57 56 sqcld ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ )
58 2cn ⊢ 2 ∈ ℂ
59 mulcom ⊢ ( ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) = ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) )
60 57 58 59 sylancl ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) = ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) )
61 60 oveq2d ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( 1 · 2 ) − ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) ) = ( ( 1 · 2 ) − ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
62 58 mulid2i ⊢ ( 1 · 2 ) = 2
63 df-2 ⊢ 2 = ( 1 + 1 )
64 62 63 eqtri ⊢ ( 1 · 2 ) = ( 1 + 1 )
65 64 oveq1i ⊢ ( ( 1 · 2 ) − ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) = ( ( 1 + 1 ) − ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) )
66 61 65 eqtrdi ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( 1 · 2 ) − ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) ) = ( ( 1 + 1 ) − ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
67 subdir ⊢ ( ( 1 ∈ ℂ ∧ ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 1 − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) · 2 ) = ( ( 1 · 2 ) − ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) ) )
68 49 58 67 mp3an13 ⊢ ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ → ( ( 1 − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) · 2 ) = ( ( 1 · 2 ) − ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) ) )
69 57 68 syl ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( 1 − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) · 2 ) = ( ( 1 · 2 ) − ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) ) )
70 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ )
71 58 57 70 sylancr ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ )
72 subsub3 ⊢ ( ( 1 ∈ ℂ ∧ ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( 1 − ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) = ( ( 1 + 1 ) − ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
73 49 49 72 mp3an13 ⊢ ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ → ( 1 − ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) = ( ( 1 + 1 ) − ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
74 71 73 syl ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( 1 − ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) = ( ( 1 + 1 ) − ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
75 66 69 74 3eqtr4d ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( 1 − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) · 2 ) = ( 1 − ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) )
76 sincl ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℂ )
77 76 sqcld ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ )
78 77 57 pncand ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) + ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
79 sincossq ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) + ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 1 )
80 79 oveq1d ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) + ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = ( 1 − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) )
81 78 80 eqtr3d ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = ( 1 − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) )
82 81 oveq1d ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) = ( ( 1 − ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) · 2 ) )
83 cos2t ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) )
84 83 oveq2d ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( 1 − ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) ) = ( 1 − ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) )
85 75 82 84 3eqtr4d ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) = ( 1 − ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) ) )
86 55 85 syl ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) = ( 1 − ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) ) )
87 2ne0 ⊢ 2 ≠ 0
88 divcan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
89 58 87 88 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
90 89 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( cos ‘ 𝐴 ) )
91 90 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) ) = ( 1 − ( cos ‘ 𝐴 ) ) )
92 86 91 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) = ( 1 − ( cos ‘ 𝐴 ) ) )
93 92 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) / 2 ) = ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) )
94 55 sincld ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℂ )
95 94 sqcld ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ )
96 divcan4 ⊢ ( ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) / 2 ) = ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
97 58 87 96 mp3an23 ⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ → ( ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) / 2 ) = ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
98 95 97 syl ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) · 2 ) / 2 ) = ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
99 54 93 98 3eqtr2rd ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = ( ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) ↑ 2 ) )
100 48 99 syl ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = ( ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) ↑ 2 ) )
101 9 24 45 47 100 sq11d ⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( sin ‘ ( 𝐴 / 2 ) ) = ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )