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