Metamath Proof Explorer

Theorem sin2h

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

Ref Expression
Assertion sin2h 
|- ( A e. ( 0 [,] ( 2 x. _pi ) ) -> ( sin ` ( A / 2 ) ) = ( sqrt ` ( ( 1 - ( cos ` A ) ) / 2 ) ) )

Proof

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