Metamath Proof Explorer


Theorem tan2h

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

Ref Expression
Assertion tan2h A 0 π tan A 2 = 1 cos A 1 + cos A

Proof

Step Hyp Ref Expression
1 0re 0
2 pire π
3 2 rexri π *
4 icossre 0 π * 0 π
5 1 3 4 mp2an 0 π
6 5 sseli A 0 π A
7 6 recnd A 0 π A
8 7 halfcld A 0 π A 2
9 6 rehalfcld A 0 π A 2
10 9 rered A 0 π A 2 = A 2
11 elico2 0 π * A 0 π A 0 A A < π
12 1 3 11 mp2an A 0 π A 0 A A < π
13 pipos 0 < π
14 lt0neg2 π 0 < π π < 0
15 2 14 ax-mp 0 < π π < 0
16 13 15 mpbi π < 0
17 2 renegcli π
18 ltletr π 0 A π < 0 0 A π < A
19 17 1 18 mp3an12 A π < 0 0 A π < A
20 16 19 mpani A 0 A π < A
21 2re 2
22 2pos 0 < 2
23 21 22 pm3.2i 2 0 < 2
24 ltdiv1 π A 2 0 < 2 π < A π 2 < A 2
25 17 23 24 mp3an13 A π < A π 2 < A 2
26 picn π
27 2cn 2
28 2ne0 2 0
29 divneg π 2 2 0 π 2 = π 2
30 26 27 28 29 mp3an π 2 = π 2
31 30 breq1i π 2 < A 2 π 2 < A 2
32 25 31 bitr4di A π < A π 2 < A 2
33 20 32 sylibd A 0 A π 2 < A 2
34 ltdiv1 A π 2 0 < 2 A < π A 2 < π 2
35 2 23 34 mp3an23 A A < π A 2 < π 2
36 35 biimpd A A < π A 2 < π 2
37 33 36 anim12d A 0 A A < π π 2 < A 2 A 2 < π 2
38 rehalfcl A A 2
39 38 rexrd A A 2 *
40 halfpire π 2
41 40 renegcli π 2
42 41 rexri π 2 *
43 40 rexri π 2 *
44 elioo5 π 2 * π 2 * A 2 * A 2 π 2 π 2 π 2 < A 2 A 2 < π 2
45 42 43 44 mp3an12 A 2 * A 2 π 2 π 2 π 2 < A 2 A 2 < π 2
46 39 45 syl A A 2 π 2 π 2 π 2 < A 2 A 2 < π 2
47 37 46 sylibrd A 0 A A < π A 2 π 2 π 2
48 47 3impib A 0 A A < π A 2 π 2 π 2
49 12 48 sylbi A 0 π A 2 π 2 π 2
50 10 49 eqeltrd A 0 π A 2 π 2 π 2
51 cosne0 A 2 A 2 π 2 π 2 cos A 2 0
52 8 50 51 syl2anc A 0 π cos A 2 0
53 tanval A 2 cos A 2 0 tan A 2 = sin A 2 cos A 2
54 8 52 53 syl2anc A 0 π tan A 2 = sin A 2 cos A 2
55 0xr 0 *
56 elico1 0 * π * A 0 π A * 0 A A < π
57 55 3 56 mp2an A 0 π A * 0 A A < π
58 21 2 remulcli 2 π
59 58 rexri 2 π *
60 1lt2 1 < 2
61 ltmulgt12 π 2 0 < π 1 < 2 π < 2 π
62 2 21 13 61 mp3an 1 < 2 π < 2 π
63 60 62 mpbi π < 2 π
64 xrlttr A * π * 2 π * A < π π < 2 π A < 2 π
65 3 64 mp3an2 A * 2 π * A < π π < 2 π A < 2 π
66 63 65 mpan2i A * 2 π * A < π A < 2 π
67 xrltle A * 2 π * A < 2 π A 2 π
68 66 67 syld A * 2 π * A < π A 2 π
69 59 68 mpan2 A * A < π A 2 π
70 69 anim2d A * 0 A A < π 0 A A 2 π
71 elicc4 0 * 2 π * A * A 0 2 π 0 A A 2 π
72 55 59 71 mp3an12 A * A 0 2 π 0 A A 2 π
73 70 72 sylibrd A * 0 A A < π A 0 2 π
74 73 3impib A * 0 A A < π A 0 2 π
75 57 74 sylbi A 0 π A 0 2 π
76 sin2h A 0 2 π sin A 2 = 1 cos A 2
77 75 76 syl A 0 π sin A 2 = 1 cos A 2
78 1 2 13 ltleii 0 π
79 le0neg2 π 0 π π 0
80 2 79 ax-mp 0 π π 0
81 78 80 mpbi π 0
82 17 rexri π *
83 xrletr π * 0 * A * π 0 0 A π A
84 82 55 83 mp3an12 A * π 0 0 A π A
85 81 84 mpani A * 0 A π A
86 xrltle A * π * A < π A π
87 3 86 mpan2 A * A < π A π
88 85 87 anim12d A * 0 A A < π π A A π
89 elicc4 π * π * A * A π π π A A π
90 82 3 89 mp3an12 A * A π π π A A π
91 88 90 sylibrd A * 0 A A < π A π π
92 91 3impib A * 0 A A < π A π π
93 57 92 sylbi A 0 π A π π
94 cos2h A π π cos A 2 = 1 + cos A 2
95 93 94 syl A 0 π cos A 2 = 1 + cos A 2
96 77 95 oveq12d A 0 π sin A 2 cos A 2 = 1 cos A 2 1 + cos A 2
97 54 96 eqtrd A 0 π tan A 2 = 1 cos A 2 1 + cos A 2
98 1re 1
99 6 recoscld A 0 π cos A
100 resubcl 1 cos A 1 cos A
101 98 99 100 sylancr A 0 π 1 cos A
102 101 rehalfcld A 0 π 1 cos A 2
103 cosbnd A 1 cos A cos A 1
104 103 simprd A cos A 1
105 recoscl A cos A
106 subge0 1 cos A 0 1 cos A cos A 1
107 halfnneg2 1 cos A 0 1 cos A 0 1 cos A 2
108 100 107 syl 1 cos A 0 1 cos A 0 1 cos A 2
109 106 108 bitr3d 1 cos A cos A 1 0 1 cos A 2
110 98 105 109 sylancr A cos A 1 0 1 cos A 2
111 104 110 mpbid A 0 1 cos A 2
112 6 111 syl A 0 π 0 1 cos A 2
113 readdcl 1 cos A 1 + cos A
114 98 99 113 sylancr A 0 π 1 + cos A
115 103 simpld A 1 cos A
116 98 renegcli 1
117 subge0 cos A 1 0 cos A -1 1 cos A
118 105 116 117 sylancl A 0 cos A -1 1 cos A
119 recn A A
120 119 coscld A cos A
121 ax-1cn 1
122 subneg cos A 1 cos A -1 = cos A + 1
123 addcom cos A 1 cos A + 1 = 1 + cos A
124 122 123 eqtrd cos A 1 cos A -1 = 1 + cos A
125 120 121 124 sylancl A cos A -1 = 1 + cos A
126 125 breq2d A 0 cos A -1 0 1 + cos A
127 118 126 bitr3d A 1 cos A 0 1 + cos A
128 115 127 mpbid A 0 1 + cos A
129 6 128 syl A 0 π 0 1 + cos A
130 snunioo 0 * π * 0 < π 0 0 π = 0 π
131 55 3 13 130 mp3an 0 0 π = 0 π
132 131 eleq2i A 0 0 π A 0 π
133 elun A 0 0 π A 0 A 0 π
134 132 133 bitr3i A 0 π A 0 A 0 π
135 elsni A 0 A = 0
136 fveq2 A = 0 cos A = cos 0
137 cos0 cos 0 = 1
138 136 137 eqtrdi A = 0 cos A = 1
139 138 oveq2d A = 0 1 + cos A = 1 + 1
140 df-2 2 = 1 + 1
141 139 140 eqtr4di A = 0 1 + cos A = 2
142 28 a1i A = 0 2 0
143 141 142 eqnetrd A = 0 1 + cos A 0
144 135 143 syl A 0 1 + cos A 0
145 sinq12gt0 A 0 π 0 < sin A
146 ltne 0 0 < sin A sin A 0
147 1 146 mpan 0 < sin A sin A 0
148 elioore A 0 π A
149 148 recnd A 0 π A
150 oveq1 1 = cos A 1 2 = cos A 2
151 150 a1i A 1 = cos A 1 2 = cos A 2
152 df-neg 1 = 0 1
153 152 eqeq1i 1 = cos A 0 1 = cos A
154 coscl A cos A
155 0cn 0
156 subadd 0 1 cos A 0 1 = cos A 1 + cos A = 0
157 155 121 156 mp3an12 cos A 0 1 = cos A 1 + cos A = 0
158 154 157 syl A 0 1 = cos A 1 + cos A = 0
159 153 158 syl5bb A 1 = cos A 1 + cos A = 0
160 sincl A sin A
161 160 sqcld A sin A 2
162 0cnd A 0
163 154 sqcld A cos A 2
164 161 162 163 addcan2d A sin A 2 + cos A 2 = 0 + cos A 2 sin A 2 = 0
165 sincossq A sin A 2 + cos A 2 = 1
166 neg1sqe1 1 2 = 1
167 165 166 eqtr4di A sin A 2 + cos A 2 = 1 2
168 163 addid2d A 0 + cos A 2 = cos A 2
169 167 168 eqeq12d A sin A 2 + cos A 2 = 0 + cos A 2 1 2 = cos A 2
170 sqeq0 sin A sin A 2 = 0 sin A = 0
171 160 170 syl A sin A 2 = 0 sin A = 0
172 164 169 171 3bitr3d A 1 2 = cos A 2 sin A = 0
173 151 159 172 3imtr3d A 1 + cos A = 0 sin A = 0
174 149 173 syl A 0 π 1 + cos A = 0 sin A = 0
175 174 necon3d A 0 π sin A 0 1 + cos A 0
176 147 175 syl5 A 0 π 0 < sin A 1 + cos A 0
177 145 176 mpd A 0 π 1 + cos A 0
178 144 177 jaoi A 0 A 0 π 1 + cos A 0
179 134 178 sylbi A 0 π 1 + cos A 0
180 114 129 179 ne0gt0d A 0 π 0 < 1 + cos A
181 114 180 elrpd A 0 π 1 + cos A +
182 181 rphalfcld A 0 π 1 + cos A 2 +
183 102 112 182 sqrtdivd A 0 π 1 cos A 2 1 + cos A 2 = 1 cos A 2 1 + cos A 2
184 7 coscld A 0 π cos A
185 subcl 1 cos A 1 cos A
186 121 184 185 sylancr A 0 π 1 cos A
187 addcl 1 cos A 1 + cos A
188 121 184 187 sylancr A 0 π 1 + cos A
189 2cnne0 2 2 0
190 divcan7 1 cos A 1 + cos A 1 + cos A 0 2 2 0 1 cos A 2 1 + cos A 2 = 1 cos A 1 + cos A
191 189 190 mp3an3 1 cos A 1 + cos A 1 + cos A 0 1 cos A 2 1 + cos A 2 = 1 cos A 1 + cos A
192 186 188 179 191 syl12anc A 0 π 1 cos A 2 1 + cos A 2 = 1 cos A 1 + cos A
193 192 fveq2d A 0 π 1 cos A 2 1 + cos A 2 = 1 cos A 1 + cos A
194 97 183 193 3eqtr2d A 0 π tan A 2 = 1 cos A 1 + cos A