Metamath Proof Explorer

Theorem cos2h

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

Ref Expression
Assertion cos2h ( 𝐴 ∈ ( - π [,] π ) → ( cos ‘ ( 𝐴 / 2 ) ) = ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )

Proof

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