Metamath Proof Explorer

Theorem cos2h

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

Ref Expression
Assertion cos2h 
|- ( A e. ( -u _pi [,] _pi ) -> ( cos ` ( A / 2 ) ) = ( sqrt ` ( ( 1 + ( cos ` A ) ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 1 renegcli 
 |-  -u _pi e. RR
3 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
4 2 1 3 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
5 4 sseli 
 |-  ( A e. ( -u _pi [,] _pi ) -> A e. RR )
6 5 rehalfcld 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( A / 2 ) e. RR )
7 6 recoscld 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( cos ` ( A / 2 ) ) e. RR )
8 1re 
 |-  1 e. RR
9 5 recoscld 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( cos ` A ) e. RR )
10 readdcl 
 |-  ( ( 1 e. RR /\ ( cos ` A ) e. RR ) -> ( 1 + ( cos ` A ) ) e. RR )
11 8 9 10 sylancr 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( 1 + ( cos ` A ) ) e. RR )
12 11 rehalfcld 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( ( 1 + ( cos ` A ) ) / 2 ) e. RR )
13 cosbnd 
 |-  ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
14 13 simpld 
 |-  ( A e. RR -> -u 1 <_ ( cos ` A ) )
15 recoscl 
 |-  ( A e. RR -> ( cos ` A ) e. RR )
16 recn 
 |-  ( ( cos ` A ) e. RR -> ( cos ` A ) e. CC )
17 recn 
 |-  ( 1 e. RR -> 1 e. CC )
18 subneg 
 |-  ( ( ( cos ` A ) e. CC /\ 1 e. CC ) -> ( ( cos ` A ) - -u 1 ) = ( ( cos ` A ) + 1 ) )
19 addcom 
 |-  ( ( 1 e. CC /\ ( cos ` A ) e. CC ) -> ( 1 + ( cos ` A ) ) = ( ( cos ` A ) + 1 ) )
20 19 ancoms 
 |-  ( ( ( cos ` A ) e. CC /\ 1 e. CC ) -> ( 1 + ( cos ` A ) ) = ( ( cos ` A ) + 1 ) )
21 18 20 eqtr4d 
 |-  ( ( ( cos ` A ) e. CC /\ 1 e. CC ) -> ( ( cos ` A ) - -u 1 ) = ( 1 + ( cos ` A ) ) )
22 16 17 21 syl2an 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR ) -> ( ( cos ` A ) - -u 1 ) = ( 1 + ( cos ` A ) ) )
23 22 breq2d 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR ) -> ( 0 <_ ( ( cos ` A ) - -u 1 ) <-> 0 <_ ( 1 + ( cos ` A ) ) ) )
24 renegcl 
 |-  ( 1 e. RR -> -u 1 e. RR )
25 subge0 
 |-  ( ( ( cos ` A ) e. RR /\ -u 1 e. RR ) -> ( 0 <_ ( ( cos ` A ) - -u 1 ) <-> -u 1 <_ ( cos ` A ) ) )
26 24 25 sylan2 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR ) -> ( 0 <_ ( ( cos ` A ) - -u 1 ) <-> -u 1 <_ ( cos ` A ) ) )
27 10 ancoms 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR ) -> ( 1 + ( cos ` A ) ) e. RR )
28 halfnneg2 
 |-  ( ( 1 + ( cos ` A ) ) e. RR -> ( 0 <_ ( 1 + ( cos ` A ) ) <-> 0 <_ ( ( 1 + ( cos ` A ) ) / 2 ) ) )
29 27 28 syl 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR ) -> ( 0 <_ ( 1 + ( cos ` A ) ) <-> 0 <_ ( ( 1 + ( cos ` A ) ) / 2 ) ) )
30 23 26 29 3bitr3d 
 |-  ( ( ( cos ` A ) e. RR /\ 1 e. RR ) -> ( -u 1 <_ ( cos ` A ) <-> 0 <_ ( ( 1 + ( cos ` A ) ) / 2 ) ) )
31 15 8 30 sylancl 
 |-  ( A e. RR -> ( -u 1 <_ ( cos ` A ) <-> 0 <_ ( ( 1 + ( cos ` A ) ) / 2 ) ) )
32 14 31 mpbid 
 |-  ( A e. RR -> 0 <_ ( ( 1 + ( cos ` A ) ) / 2 ) )
33 5 32 syl 
 |-  ( A e. ( -u _pi [,] _pi ) -> 0 <_ ( ( 1 + ( cos ` A ) ) / 2 ) )
34 12 33 resqrtcld 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( sqrt ` ( ( 1 + ( cos ` A ) ) / 2 ) ) e. RR )
35 2 1 elicc2i 
 |-  ( A e. ( -u _pi [,] _pi ) <-> ( A e. RR /\ -u _pi <_ A /\ A <_ _pi ) )
36 2re 
 |-  2 e. RR
37 2pos 
 |-  0 < 2
38 36 37 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
39 lediv1 
 |-  ( ( -u _pi e. RR /\ A e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( -u _pi <_ A <-> ( -u _pi / 2 ) <_ ( A / 2 ) ) )
40 2 38 39 mp3an13 
 |-  ( A e. RR -> ( -u _pi <_ A <-> ( -u _pi / 2 ) <_ ( A / 2 ) ) )
41 picn 
 |-  _pi e. CC
42 2cn 
 |-  2 e. CC
43 2ne0 
 |-  2 =/= 0
44 divneg 
 |-  ( ( _pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( _pi / 2 ) = ( -u _pi / 2 ) )
45 41 42 43 44 mp3an 
 |-  -u ( _pi / 2 ) = ( -u _pi / 2 )
46 45 breq1i 
 |-  ( -u ( _pi / 2 ) <_ ( A / 2 ) <-> ( -u _pi / 2 ) <_ ( A / 2 ) )
47 40 46 bitr4di 
 |-  ( A e. RR -> ( -u _pi <_ A <-> -u ( _pi / 2 ) <_ ( A / 2 ) ) )
48 lediv1 
 |-  ( ( A e. RR /\ _pi e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( A <_ _pi <-> ( A / 2 ) <_ ( _pi / 2 ) ) )
49 1 38 48 mp3an23 
 |-  ( A e. RR -> ( A <_ _pi <-> ( A / 2 ) <_ ( _pi / 2 ) ) )
50 47 49 anbi12d 
 |-  ( A e. RR -> ( ( -u _pi <_ A /\ A <_ _pi ) <-> ( -u ( _pi / 2 ) <_ ( A / 2 ) /\ ( A / 2 ) <_ ( _pi / 2 ) ) ) )
51 rehalfcl 
 |-  ( A e. RR -> ( A / 2 ) e. RR )
52 51 rexrd 
 |-  ( A e. RR -> ( A / 2 ) e. RR* )
53 halfpire 
 |-  ( _pi / 2 ) e. RR
54 53 renegcli 
 |-  -u ( _pi / 2 ) e. RR
55 54 rexri 
 |-  -u ( _pi / 2 ) e. RR*
56 53 rexri 
 |-  ( _pi / 2 ) e. RR*
57 elicc4 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* /\ ( A / 2 ) e. RR* ) -> ( ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( -u ( _pi / 2 ) <_ ( A / 2 ) /\ ( A / 2 ) <_ ( _pi / 2 ) ) ) )
58 55 56 57 mp3an12 
 |-  ( ( A / 2 ) e. RR* -> ( ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( -u ( _pi / 2 ) <_ ( A / 2 ) /\ ( A / 2 ) <_ ( _pi / 2 ) ) ) )
59 52 58 syl 
 |-  ( A e. RR -> ( ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( -u ( _pi / 2 ) <_ ( A / 2 ) /\ ( A / 2 ) <_ ( _pi / 2 ) ) ) )
60 50 59 bitr4d 
 |-  ( A e. RR -> ( ( -u _pi <_ A /\ A <_ _pi ) <-> ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) )
61 60 biimpd 
 |-  ( A e. RR -> ( ( -u _pi <_ A /\ A <_ _pi ) -> ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) )
62 61 3impib 
 |-  ( ( A e. RR /\ -u _pi <_ A /\ A <_ _pi ) -> ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
63 35 62 sylbi 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
64 cosq14ge0 
 |-  ( ( A / 2 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( cos ` ( A / 2 ) ) )
65 63 64 syl 
 |-  ( A e. ( -u _pi [,] _pi ) -> 0 <_ ( cos ` ( A / 2 ) ) )
66 12 33 sqrtge0d 
 |-  ( A e. ( -u _pi [,] _pi ) -> 0 <_ ( sqrt ` ( ( 1 + ( cos ` A ) ) / 2 ) ) )
67 5 recnd 
 |-  ( A e. ( -u _pi [,] _pi ) -> A e. CC )
68 ax-1cn 
 |-  1 e. CC
69 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
70 addcl 
 |-  ( ( 1 e. CC /\ ( cos ` A ) e. CC ) -> ( 1 + ( cos ` A ) ) e. CC )
71 68 69 70 sylancr 
 |-  ( A e. CC -> ( 1 + ( cos ` A ) ) e. CC )
72 71 halfcld 
 |-  ( A e. CC -> ( ( 1 + ( cos ` A ) ) / 2 ) e. CC )
73 72 sqsqrtd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( 1 + ( cos ` A ) ) / 2 ) ) ^ 2 ) = ( ( 1 + ( cos ` A ) ) / 2 ) )
74 divcan2 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( A / 2 ) ) = A )
75 42 43 74 mp3an23 
 |-  ( A e. CC -> ( 2 x. ( A / 2 ) ) = A )
76 75 fveq2d 
 |-  ( A e. CC -> ( cos ` ( 2 x. ( A / 2 ) ) ) = ( cos ` A ) )
77 halfcl 
 |-  ( A e. CC -> ( A / 2 ) e. CC )
78 cos2t 
 |-  ( ( A / 2 ) e. CC -> ( cos ` ( 2 x. ( A / 2 ) ) ) = ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) )
79 77 78 syl 
 |-  ( A e. CC -> ( cos ` ( 2 x. ( A / 2 ) ) ) = ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) )
80 76 79 eqtr3d 
 |-  ( A e. CC -> ( cos ` A ) = ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) )
81 80 oveq2d 
 |-  ( A e. CC -> ( 1 + ( cos ` A ) ) = ( 1 + ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) ) )
82 81 oveq1d 
 |-  ( A e. CC -> ( ( 1 + ( cos ` A ) ) / 2 ) = ( ( 1 + ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) ) / 2 ) )
83 77 coscld 
 |-  ( A e. CC -> ( cos ` ( A / 2 ) ) e. CC )
84 83 sqcld 
 |-  ( A e. CC -> ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC )
85 mulcl 
 |-  ( ( 2 e. CC /\ ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC ) -> ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) e. CC )
86 42 85 mpan 
 |-  ( ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC -> ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) e. CC )
87 pncan3 
 |-  ( ( 1 e. CC /\ ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) e. CC ) -> ( 1 + ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) ) = ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) )
88 68 86 87 sylancr 
 |-  ( ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC -> ( 1 + ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) ) = ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) )
89 88 oveq1d 
 |-  ( ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC -> ( ( 1 + ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) ) / 2 ) = ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) / 2 ) )
90 divcan3 
 |-  ( ( ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) / 2 ) = ( ( cos ` ( A / 2 ) ) ^ 2 ) )
91 42 43 90 mp3an23 
 |-  ( ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC -> ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) / 2 ) = ( ( cos ` ( A / 2 ) ) ^ 2 ) )
92 89 91 eqtrd 
 |-  ( ( ( cos ` ( A / 2 ) ) ^ 2 ) e. CC -> ( ( 1 + ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) ) / 2 ) = ( ( cos ` ( A / 2 ) ) ^ 2 ) )
93 84 92 syl 
 |-  ( A e. CC -> ( ( 1 + ( ( 2 x. ( ( cos ` ( A / 2 ) ) ^ 2 ) ) - 1 ) ) / 2 ) = ( ( cos ` ( A / 2 ) ) ^ 2 ) )
94 73 82 93 3eqtrrd 
 |-  ( A e. CC -> ( ( cos ` ( A / 2 ) ) ^ 2 ) = ( ( sqrt ` ( ( 1 + ( cos ` A ) ) / 2 ) ) ^ 2 ) )
95 67 94 syl 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( ( cos ` ( A / 2 ) ) ^ 2 ) = ( ( sqrt ` ( ( 1 + ( cos ` A ) ) / 2 ) ) ^ 2 ) )
96 7 34 65 66 95 sq11d 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( cos ` ( A / 2 ) ) = ( sqrt ` ( ( 1 + ( cos ` A ) ) / 2 ) ) )