Metamath Proof Explorer


Theorem tan2h

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

Ref Expression
Assertion tan2h A0πtanA2=1cosA1+cosA

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 A0πA
7 6 recnd A0πA
8 7 halfcld A0πA2
9 6 rehalfcld A0πA2
10 9 rered A0πA2=A2
11 elico2 0π*A0πA0AA<π
12 1 3 11 mp2an A0πA0AA<π
13 pipos 0<π
14 lt0neg2 π0<ππ<0
15 2 14 ax-mp 0<ππ<0
16 13 15 mpbi π<0
17 2 renegcli π
18 ltletr π0Aπ<00Aπ<A
19 17 1 18 mp3an12 Aπ<00Aπ<A
20 16 19 mpani A0Aπ<A
21 2re 2
22 2pos 0<2
23 21 22 pm3.2i 20<2
24 ltdiv1 πA20<2π<Aπ2<A2
25 17 23 24 mp3an13 Aπ<Aπ2<A2
26 picn π
27 2cn 2
28 2ne0 20
29 divneg π220π2=π2
30 26 27 28 29 mp3an π2=π2
31 30 breq1i π2<A2π2<A2
32 25 31 bitr4di Aπ<Aπ2<A2
33 20 32 sylibd A0Aπ2<A2
34 ltdiv1 Aπ20<2A<πA2<π2
35 2 23 34 mp3an23 AA<πA2<π2
36 35 biimpd AA<πA2<π2
37 33 36 anim12d A0AA<ππ2<A2A2<π2
38 rehalfcl AA2
39 38 rexrd AA2*
40 halfpire π2
41 40 renegcli π2
42 41 rexri π2*
43 40 rexri π2*
44 elioo5 π2*π2*A2*A2π2π2π2<A2A2<π2
45 42 43 44 mp3an12 A2*A2π2π2π2<A2A2<π2
46 39 45 syl AA2π2π2π2<A2A2<π2
47 37 46 sylibrd A0AA<πA2π2π2
48 47 3impib A0AA<πA2π2π2
49 12 48 sylbi A0πA2π2π2
50 10 49 eqeltrd A0πA2π2π2
51 cosne0 A2A2π2π2cosA20
52 8 50 51 syl2anc A0πcosA20
53 tanval A2cosA20tanA2=sinA2cosA2
54 8 52 53 syl2anc A0πtanA2=sinA2cosA2
55 0xr 0*
56 elico1 0*π*A0πA*0AA<π
57 55 3 56 mp2an A0πA*0AA<π
58 21 2 remulcli 2π
59 58 rexri 2π*
60 1lt2 1<2
61 ltmulgt12 π20<π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πA2π
68 66 67 syld A*2π*A<πA2π
69 59 68 mpan2 A*A<πA2π
70 69 anim2d A*0AA<π0AA2π
71 elicc4 0*2π*A*A02π0AA2π
72 55 59 71 mp3an12 A*A02π0AA2π
73 70 72 sylibrd A*0AA<πA02π
74 73 3impib A*0AA<πA02π
75 57 74 sylbi A0πA02π
76 sin2h A02πsinA2=1cosA2
77 75 76 syl A0πsinA2=1cosA2
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*π00AπA
84 82 55 83 mp3an12 A*π00AπA
85 81 84 mpani A*0AπA
86 xrltle A*π*A<πAπ
87 3 86 mpan2 A*A<πAπ
88 85 87 anim12d A*0AA<ππAAπ
89 elicc4 π*π*A*AπππAAπ
90 82 3 89 mp3an12 A*AπππAAπ
91 88 90 sylibrd A*0AA<πAππ
92 91 3impib A*0AA<πAππ
93 57 92 sylbi A0πAππ
94 cos2h AππcosA2=1+cosA2
95 93 94 syl A0πcosA2=1+cosA2
96 77 95 oveq12d A0πsinA2cosA2=1cosA21+cosA2
97 54 96 eqtrd A0πtanA2=1cosA21+cosA2
98 1re 1
99 6 recoscld A0πcosA
100 resubcl 1cosA1cosA
101 98 99 100 sylancr A0π1cosA
102 101 rehalfcld A0π1cosA2
103 cosbnd A1cosAcosA1
104 103 simprd AcosA1
105 recoscl AcosA
106 subge0 1cosA01cosAcosA1
107 halfnneg2 1cosA01cosA01cosA2
108 100 107 syl 1cosA01cosA01cosA2
109 106 108 bitr3d 1cosAcosA101cosA2
110 98 105 109 sylancr AcosA101cosA2
111 104 110 mpbid A01cosA2
112 6 111 syl A0π01cosA2
113 readdcl 1cosA1+cosA
114 98 99 113 sylancr A0π1+cosA
115 103 simpld A1cosA
116 98 renegcli 1
117 subge0 cosA10cosA-11cosA
118 105 116 117 sylancl A0cosA-11cosA
119 recn AA
120 119 coscld AcosA
121 ax-1cn 1
122 subneg cosA1cosA-1=cosA+1
123 addcom cosA1cosA+1=1+cosA
124 122 123 eqtrd cosA1cosA-1=1+cosA
125 120 121 124 sylancl AcosA-1=1+cosA
126 125 breq2d A0cosA-101+cosA
127 118 126 bitr3d A1cosA01+cosA
128 115 127 mpbid A01+cosA
129 6 128 syl A0π01+cosA
130 snunioo 0*π*0<π00π=0π
131 55 3 13 130 mp3an 00π=0π
132 131 eleq2i A00πA0π
133 elun A00πA0A0π
134 132 133 bitr3i A0πA0A0π
135 elsni A0A=0
136 fveq2 A=0cosA=cos0
137 cos0 cos0=1
138 136 137 eqtrdi A=0cosA=1
139 138 oveq2d A=01+cosA=1+1
140 df-2 2=1+1
141 139 140 eqtr4di A=01+cosA=2
142 28 a1i A=020
143 141 142 eqnetrd A=01+cosA0
144 135 143 syl A01+cosA0
145 sinq12gt0 A0π0<sinA
146 ltne 00<sinAsinA0
147 1 146 mpan 0<sinAsinA0
148 elioore A0πA
149 148 recnd A0πA
150 oveq1 1=cosA12=cosA2
151 150 a1i A1=cosA12=cosA2
152 df-neg 1=01
153 152 eqeq1i 1=cosA01=cosA
154 coscl AcosA
155 0cn 0
156 subadd 01cosA01=cosA1+cosA=0
157 155 121 156 mp3an12 cosA01=cosA1+cosA=0
158 154 157 syl A01=cosA1+cosA=0
159 153 158 syl5bb A1=cosA1+cosA=0
160 sincl AsinA
161 160 sqcld AsinA2
162 0cnd A0
163 154 sqcld AcosA2
164 161 162 163 addcan2d AsinA2+cosA2=0+cosA2sinA2=0
165 sincossq AsinA2+cosA2=1
166 neg1sqe1 12=1
167 165 166 eqtr4di AsinA2+cosA2=12
168 163 addid2d A0+cosA2=cosA2
169 167 168 eqeq12d AsinA2+cosA2=0+cosA212=cosA2
170 sqeq0 sinAsinA2=0sinA=0
171 160 170 syl AsinA2=0sinA=0
172 164 169 171 3bitr3d A12=cosA2sinA=0
173 151 159 172 3imtr3d A1+cosA=0sinA=0
174 149 173 syl A0π1+cosA=0sinA=0
175 174 necon3d A0πsinA01+cosA0
176 147 175 syl5 A0π0<sinA1+cosA0
177 145 176 mpd A0π1+cosA0
178 144 177 jaoi A0A0π1+cosA0
179 134 178 sylbi A0π1+cosA0
180 114 129 179 ne0gt0d A0π0<1+cosA
181 114 180 elrpd A0π1+cosA+
182 181 rphalfcld A0π1+cosA2+
183 102 112 182 sqrtdivd A0π1cosA21+cosA2=1cosA21+cosA2
184 7 coscld A0πcosA
185 subcl 1cosA1cosA
186 121 184 185 sylancr A0π1cosA
187 addcl 1cosA1+cosA
188 121 184 187 sylancr A0π1+cosA
189 2cnne0 220
190 divcan7 1cosA1+cosA1+cosA02201cosA21+cosA2=1cosA1+cosA
191 189 190 mp3an3 1cosA1+cosA1+cosA01cosA21+cosA2=1cosA1+cosA
192 186 188 179 191 syl12anc A0π1cosA21+cosA2=1cosA1+cosA
193 192 fveq2d A0π1cosA21+cosA2=1cosA1+cosA
194 97 183 193 3eqtr2d A0πtanA2=1cosA1+cosA