Metamath Proof Explorer


Theorem atantan

Description: The arctangent function is an inverse to tan . (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atantan A A π 2 π 2 arctan tan A = A

Proof

Step Hyp Ref Expression
1 cosne0 A A π 2 π 2 cos A 0
2 atandmtan A cos A 0 tan A dom arctan
3 1 2 syldan A A π 2 π 2 tan A dom arctan
4 atanval tan A dom arctan arctan tan A = i 2 log 1 i tan A log 1 + i tan A
5 3 4 syl A A π 2 π 2 arctan tan A = i 2 log 1 i tan A log 1 + i tan A
6 ax-1cn 1
7 ax-icn i
8 tancl A cos A 0 tan A
9 1 8 syldan A A π 2 π 2 tan A
10 mulcl i tan A i tan A
11 7 9 10 sylancr A A π 2 π 2 i tan A
12 addcl 1 i tan A 1 + i tan A
13 6 11 12 sylancr A A π 2 π 2 1 + i tan A
14 atandm2 tan A dom arctan tan A 1 i tan A 0 1 + i tan A 0
15 3 14 sylib A A π 2 π 2 tan A 1 i tan A 0 1 + i tan A 0
16 15 simp3d A A π 2 π 2 1 + i tan A 0
17 13 16 logcld A A π 2 π 2 log 1 + i tan A
18 subcl 1 i tan A 1 i tan A
19 6 11 18 sylancr A A π 2 π 2 1 i tan A
20 15 simp2d A A π 2 π 2 1 i tan A 0
21 19 20 logcld A A π 2 π 2 log 1 i tan A
22 17 21 negsubdi2d A A π 2 π 2 log 1 + i tan A log 1 i tan A = log 1 i tan A log 1 + i tan A
23 efsub log 1 + i tan A log 1 i tan A e log 1 + i tan A log 1 i tan A = e log 1 + i tan A e log 1 i tan A
24 17 21 23 syl2anc A A π 2 π 2 e log 1 + i tan A log 1 i tan A = e log 1 + i tan A e log 1 i tan A
25 coscl A cos A
26 25 adantr A A π 2 π 2 cos A
27 sincl A sin A
28 27 adantr A A π 2 π 2 sin A
29 mulcl i sin A i sin A
30 7 28 29 sylancr A A π 2 π 2 i sin A
31 26 30 26 1 divdird A A π 2 π 2 cos A + i sin A cos A = cos A cos A + i sin A cos A
32 26 1 dividd A A π 2 π 2 cos A cos A = 1
33 7 a1i A A π 2 π 2 i
34 33 28 26 1 divassd A A π 2 π 2 i sin A cos A = i sin A cos A
35 tanval A cos A 0 tan A = sin A cos A
36 1 35 syldan A A π 2 π 2 tan A = sin A cos A
37 36 oveq2d A A π 2 π 2 i tan A = i sin A cos A
38 34 37 eqtr4d A A π 2 π 2 i sin A cos A = i tan A
39 32 38 oveq12d A A π 2 π 2 cos A cos A + i sin A cos A = 1 + i tan A
40 31 39 eqtrd A A π 2 π 2 cos A + i sin A cos A = 1 + i tan A
41 efival A e i A = cos A + i sin A
42 41 adantr A A π 2 π 2 e i A = cos A + i sin A
43 42 oveq1d A A π 2 π 2 e i A cos A = cos A + i sin A cos A
44 eflog 1 + i tan A 1 + i tan A 0 e log 1 + i tan A = 1 + i tan A
45 13 16 44 syl2anc A A π 2 π 2 e log 1 + i tan A = 1 + i tan A
46 40 43 45 3eqtr4d A A π 2 π 2 e i A cos A = e log 1 + i tan A
47 26 30 26 1 divsubdird A A π 2 π 2 cos A i sin A cos A = cos A cos A i sin A cos A
48 32 38 oveq12d A A π 2 π 2 cos A cos A i sin A cos A = 1 i tan A
49 47 48 eqtrd A A π 2 π 2 cos A i sin A cos A = 1 i tan A
50 negcl A A
51 50 adantr A A π 2 π 2 A
52 efival A e i A = cos A + i sin A
53 51 52 syl A A π 2 π 2 e i A = cos A + i sin A
54 cosneg A cos A = cos A
55 54 adantr A A π 2 π 2 cos A = cos A
56 sinneg A sin A = sin A
57 56 adantr A A π 2 π 2 sin A = sin A
58 57 oveq2d A A π 2 π 2 i sin A = i sin A
59 mulneg2 i sin A i sin A = i sin A
60 7 28 59 sylancr A A π 2 π 2 i sin A = i sin A
61 58 60 eqtrd A A π 2 π 2 i sin A = i sin A
62 55 61 oveq12d A A π 2 π 2 cos A + i sin A = cos A + i sin A
63 53 62 eqtrd A A π 2 π 2 e i A = cos A + i sin A
64 simpl A A π 2 π 2 A
65 mulneg2 i A i A = i A
66 7 64 65 sylancr A A π 2 π 2 i A = i A
67 66 fveq2d A A π 2 π 2 e i A = e i A
68 26 30 negsubd A A π 2 π 2 cos A + i sin A = cos A i sin A
69 63 67 68 3eqtr3d A A π 2 π 2 e i A = cos A i sin A
70 69 oveq1d A A π 2 π 2 e i A cos A = cos A i sin A cos A
71 eflog 1 i tan A 1 i tan A 0 e log 1 i tan A = 1 i tan A
72 19 20 71 syl2anc A A π 2 π 2 e log 1 i tan A = 1 i tan A
73 49 70 72 3eqtr4d A A π 2 π 2 e i A cos A = e log 1 i tan A
74 46 73 oveq12d A A π 2 π 2 e i A cos A e i A cos A = e log 1 + i tan A e log 1 i tan A
75 mulcl i A i A
76 7 64 75 sylancr A A π 2 π 2 i A
77 efcl i A e i A
78 76 77 syl A A π 2 π 2 e i A
79 76 negcld A A π 2 π 2 i A
80 efcl i A e i A
81 79 80 syl A A π 2 π 2 e i A
82 efne0 i A e i A 0
83 79 82 syl A A π 2 π 2 e i A 0
84 78 81 26 83 1 divcan7d A A π 2 π 2 e i A cos A e i A cos A = e i A e i A
85 efsub i A i A e i A i A = e i A e i A
86 76 79 85 syl2anc A A π 2 π 2 e i A i A = e i A e i A
87 76 76 subnegd A A π 2 π 2 i A i A = i A + i A
88 76 2timesd A A π 2 π 2 2 i A = i A + i A
89 87 88 eqtr4d A A π 2 π 2 i A i A = 2 i A
90 89 fveq2d A A π 2 π 2 e i A i A = e 2 i A
91 84 86 90 3eqtr2d A A π 2 π 2 e i A cos A e i A cos A = e 2 i A
92 24 74 91 3eqtr2d A A π 2 π 2 e log 1 + i tan A log 1 i tan A = e 2 i A
93 92 fveq2d A A π 2 π 2 log e log 1 + i tan A log 1 i tan A = log e 2 i A
94 64 adantr A A π 2 π 2 A < 0 A
95 94 renegd A A π 2 π 2 A < 0 A = A
96 94 recld A A π 2 π 2 A < 0 A
97 96 renegcld A A π 2 π 2 A < 0 A
98 simpr A A π 2 π 2 A < 0 A < 0
99 96 lt0neg1d A A π 2 π 2 A < 0 A < 0 0 < A
100 98 99 mpbid A A π 2 π 2 A < 0 0 < A
101 eliooord A π 2 π 2 π 2 < A A < π 2
102 101 adantl A A π 2 π 2 π 2 < A A < π 2
103 102 simpld A A π 2 π 2 π 2 < A
104 103 adantr A A π 2 π 2 A < 0 π 2 < A
105 halfpire π 2
106 ltnegcon1 π 2 A π 2 < A A < π 2
107 105 96 106 sylancr A A π 2 π 2 A < 0 π 2 < A A < π 2
108 104 107 mpbid A A π 2 π 2 A < 0 A < π 2
109 0xr 0 *
110 105 rexri π 2 *
111 elioo2 0 * π 2 * A 0 π 2 A 0 < A A < π 2
112 109 110 111 mp2an A 0 π 2 A 0 < A A < π 2
113 97 100 108 112 syl3anbrc A A π 2 π 2 A < 0 A 0 π 2
114 95 113 eqeltrd A A π 2 π 2 A < 0 A 0 π 2
115 tanregt0 A A 0 π 2 0 < tan A
116 51 114 115 syl2an2r A A π 2 π 2 A < 0 0 < tan A
117 tanneg A cos A 0 tan A = tan A
118 1 117 syldan A A π 2 π 2 tan A = tan A
119 118 adantr A A π 2 π 2 A < 0 tan A = tan A
120 119 fveq2d A A π 2 π 2 A < 0 tan A = tan A
121 9 adantr A A π 2 π 2 A < 0 tan A
122 121 renegd A A π 2 π 2 A < 0 tan A = tan A
123 120 122 eqtrd A A π 2 π 2 A < 0 tan A = tan A
124 116 123 breqtrd A A π 2 π 2 A < 0 0 < tan A
125 9 recld A A π 2 π 2 tan A
126 125 adantr A A π 2 π 2 A < 0 tan A
127 126 lt0neg1d A A π 2 π 2 A < 0 tan A < 0 0 < tan A
128 124 127 mpbird A A π 2 π 2 A < 0 tan A < 0
129 128 lt0ne0d A A π 2 π 2 A < 0 tan A 0
130 atanlogsub tan A dom arctan tan A 0 log 1 + i tan A log 1 i tan A ran log
131 3 129 130 syl2an2r A A π 2 π 2 A < 0 log 1 + i tan A log 1 i tan A ran log
132 1re 1
133 ioossre 1 1
134 7 a1i A A π 2 π 2 A = 0 i
135 11 adantr A A π 2 π 2 A = 0 i tan A
136 ine0 i 0
137 136 a1i A A π 2 π 2 A = 0 i 0
138 ixi i i = 1
139 138 oveq1i i i tan A = -1 tan A
140 9 adantr A A π 2 π 2 A = 0 tan A
141 140 mulm1d A A π 2 π 2 A = 0 -1 tan A = tan A
142 118 adantr A A π 2 π 2 A = 0 tan A = tan A
143 141 142 eqtr4d A A π 2 π 2 A = 0 -1 tan A = tan A
144 139 143 syl5eq A A π 2 π 2 A = 0 i i tan A = tan A
145 134 134 140 mulassd A A π 2 π 2 A = 0 i i tan A = i i tan A
146 138 oveq1i i i A = -1 A
147 64 adantr A A π 2 π 2 A = 0 A
148 147 mulm1d A A π 2 π 2 A = 0 -1 A = A
149 146 148 syl5eq A A π 2 π 2 A = 0 i i A = A
150 134 134 147 mulassd A A π 2 π 2 A = 0 i i A = i i A
151 149 150 eqtr3d A A π 2 π 2 A = 0 A = i i A
152 151 fveq2d A A π 2 π 2 A = 0 tan A = tan i i A
153 144 145 152 3eqtr3d A A π 2 π 2 A = 0 i i tan A = tan i i A
154 134 135 137 153 mvllmuld A A π 2 π 2 A = 0 i tan A = tan i i A i
155 76 adantr A A π 2 π 2 A = 0 i A
156 reim A A = i A
157 156 adantr A A π 2 π 2 A = i A
158 157 eqeq1d A A π 2 π 2 A = 0 i A = 0
159 158 biimpa A A π 2 π 2 A = 0 i A = 0
160 155 159 reim0bd A A π 2 π 2 A = 0 i A
161 tanhbnd i A tan i i A i 1 1
162 160 161 syl A A π 2 π 2 A = 0 tan i i A i 1 1
163 154 162 eqeltrd A A π 2 π 2 A = 0 i tan A 1 1
164 133 163 sselid A A π 2 π 2 A = 0 i tan A
165 readdcl 1 i tan A 1 + i tan A
166 132 164 165 sylancr A A π 2 π 2 A = 0 1 + i tan A
167 df-neg 1 = 0 1
168 eliooord i tan A 1 1 1 < i tan A i tan A < 1
169 163 168 syl A A π 2 π 2 A = 0 1 < i tan A i tan A < 1
170 169 simpld A A π 2 π 2 A = 0 1 < i tan A
171 167 170 eqbrtrrid A A π 2 π 2 A = 0 0 1 < i tan A
172 0red A A π 2 π 2 A = 0 0
173 132 a1i A A π 2 π 2 A = 0 1
174 172 173 164 ltsubadd2d A A π 2 π 2 A = 0 0 1 < i tan A 0 < 1 + i tan A
175 171 174 mpbid A A π 2 π 2 A = 0 0 < 1 + i tan A
176 166 175 elrpd A A π 2 π 2 A = 0 1 + i tan A +
177 176 relogcld A A π 2 π 2 A = 0 log 1 + i tan A
178 169 simprd A A π 2 π 2 A = 0 i tan A < 1
179 difrp i tan A 1 i tan A < 1 1 i tan A +
180 164 132 179 sylancl A A π 2 π 2 A = 0 i tan A < 1 1 i tan A +
181 178 180 mpbid A A π 2 π 2 A = 0 1 i tan A +
182 181 relogcld A A π 2 π 2 A = 0 log 1 i tan A
183 177 182 resubcld A A π 2 π 2 A = 0 log 1 + i tan A log 1 i tan A
184 relogrn log 1 + i tan A log 1 i tan A log 1 + i tan A log 1 i tan A ran log
185 183 184 syl A A π 2 π 2 A = 0 log 1 + i tan A log 1 i tan A ran log
186 64 adantr A A π 2 π 2 0 < A A
187 186 recld A A π 2 π 2 0 < A A
188 simpr A A π 2 π 2 0 < A 0 < A
189 102 simprd A A π 2 π 2 A < π 2
190 189 adantr A A π 2 π 2 0 < A A < π 2
191 elioo2 0 * π 2 * A 0 π 2 A 0 < A A < π 2
192 109 110 191 mp2an A 0 π 2 A 0 < A A < π 2
193 187 188 190 192 syl3anbrc A A π 2 π 2 0 < A A 0 π 2
194 tanregt0 A A 0 π 2 0 < tan A
195 64 193 194 syl2an2r A A π 2 π 2 0 < A 0 < tan A
196 195 gt0ne0d A A π 2 π 2 0 < A tan A 0
197 3 196 130 syl2an2r A A π 2 π 2 0 < A log 1 + i tan A log 1 i tan A ran log
198 recl A A
199 198 adantr A A π 2 π 2 A
200 0re 0
201 lttri4 A 0 A < 0 A = 0 0 < A
202 199 200 201 sylancl A A π 2 π 2 A < 0 A = 0 0 < A
203 131 185 197 202 mpjao3dan A A π 2 π 2 log 1 + i tan A log 1 i tan A ran log
204 logef log 1 + i tan A log 1 i tan A ran log log e log 1 + i tan A log 1 i tan A = log 1 + i tan A log 1 i tan A
205 203 204 syl A A π 2 π 2 log e log 1 + i tan A log 1 i tan A = log 1 + i tan A log 1 i tan A
206 2cn 2
207 mulcl 2 i A 2 i A
208 206 76 207 sylancr A A π 2 π 2 2 i A
209 picn π
210 2ne0 2 0
211 divneg π 2 2 0 π 2 = π 2
212 209 206 210 211 mp3an π 2 = π 2
213 212 103 eqbrtrrid A A π 2 π 2 π 2 < A
214 pire π
215 214 renegcli π
216 215 a1i A A π 2 π 2 π
217 2re 2
218 217 a1i A A π 2 π 2 2
219 2pos 0 < 2
220 219 a1i A A π 2 π 2 0 < 2
221 ltdivmul π A 2 0 < 2 π 2 < A π < 2 A
222 216 199 218 220 221 syl112anc A A π 2 π 2 π 2 < A π < 2 A
223 213 222 mpbid A A π 2 π 2 π < 2 A
224 immul2 2 i A 2 i A = 2 i A
225 217 76 224 sylancr A A π 2 π 2 2 i A = 2 i A
226 157 oveq2d A A π 2 π 2 2 A = 2 i A
227 225 226 eqtr4d A A π 2 π 2 2 i A = 2 A
228 223 227 breqtrrd A A π 2 π 2 π < 2 i A
229 remulcl 2 A 2 A
230 217 199 229 sylancr A A π 2 π 2 2 A
231 214 a1i A A π 2 π 2 π
232 ltmuldiv2 A π 2 0 < 2 2 A < π A < π 2
233 199 231 218 220 232 syl112anc A A π 2 π 2 2 A < π A < π 2
234 189 233 mpbird A A π 2 π 2 2 A < π
235 230 231 234 ltled A A π 2 π 2 2 A π
236 227 235 eqbrtrd A A π 2 π 2 2 i A π
237 ellogrn 2 i A ran log 2 i A π < 2 i A 2 i A π
238 208 228 236 237 syl3anbrc A A π 2 π 2 2 i A ran log
239 logef 2 i A ran log log e 2 i A = 2 i A
240 238 239 syl A A π 2 π 2 log e 2 i A = 2 i A
241 93 205 240 3eqtr3d A A π 2 π 2 log 1 + i tan A log 1 i tan A = 2 i A
242 241 negeqd A A π 2 π 2 log 1 + i tan A log 1 i tan A = 2 i A
243 22 242 eqtr3d A A π 2 π 2 log 1 i tan A log 1 + i tan A = 2 i A
244 243 oveq2d A A π 2 π 2 i 2 log 1 i tan A log 1 + i tan A = i 2 2 i A
245 halfcl i i 2
246 7 245 mp1i A A π 2 π 2 i 2
247 206 a1i A A π 2 π 2 2
248 246 247 79 mulassd A A π 2 π 2 i 2 2 i A = i 2 2 i A
249 7 206 210 divcan1i i 2 2 = i
250 249 oveq1i i 2 2 i A = i i A
251 33 33 51 mulassd A A π 2 π 2 i i A = i i A
252 138 oveq1i i i A = -1 A
253 mul2neg 1 A -1 A = 1 A
254 6 64 253 sylancr A A π 2 π 2 -1 A = 1 A
255 mulid2 A 1 A = A
256 255 adantr A A π 2 π 2 1 A = A
257 254 256 eqtrd A A π 2 π 2 -1 A = A
258 252 257 syl5eq A A π 2 π 2 i i A = A
259 66 oveq2d A A π 2 π 2 i i A = i i A
260 251 258 259 3eqtr3rd A A π 2 π 2 i i A = A
261 250 260 syl5eq A A π 2 π 2 i 2 2 i A = A
262 mulneg2 2 i A 2 i A = 2 i A
263 206 76 262 sylancr A A π 2 π 2 2 i A = 2 i A
264 263 oveq2d A A π 2 π 2 i 2 2 i A = i 2 2 i A
265 248 261 264 3eqtr3rd A A π 2 π 2 i 2 2 i A = A
266 5 244 265 3eqtrd A A π 2 π 2 arctan tan A = A