# Metamath Proof Explorer

## Theorem cos2h

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

Ref Expression
Assertion cos2h $⊢ A ∈ − π π → cos ⁡ A 2 = 1 + cos ⁡ A 2$

### Proof

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