Metamath Proof Explorer

Theorem dvatan

Description: The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypotheses atansopn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
atansopn.s 
|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
Assertion dvatan 
|- ( CC _D ( arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 atansopn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 atansopn.s 
 |-  S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
3 cnelprrecn 
 |-  CC e. { RR , CC }
4 3 a1i 
 |-  ( T. -> CC e. { RR , CC } )
5 ax-1cn 
 |-  1 e. CC
6 ax-icn 
 |-  _i e. CC
7 1 2 atansssdm 
 |-  S C_ dom arctan
8 simpr 
 |-  ( ( T. /\ x e. S ) -> x e. S )
9 7 8 sselid 
 |-  ( ( T. /\ x e. S ) -> x e. dom arctan )
10 atandm2 
 |-  ( x e. dom arctan <-> ( x e. CC /\ ( 1 - ( _i x. x ) ) =/= 0 /\ ( 1 + ( _i x. x ) ) =/= 0 ) )
11 9 10 sylib 
 |-  ( ( T. /\ x e. S ) -> ( x e. CC /\ ( 1 - ( _i x. x ) ) =/= 0 /\ ( 1 + ( _i x. x ) ) =/= 0 ) )
12 11 simp1d 
 |-  ( ( T. /\ x e. S ) -> x e. CC )
13 mulcl 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
14 6 12 13 sylancr 
 |-  ( ( T. /\ x e. S ) -> ( _i x. x ) e. CC )
15 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 - ( _i x. x ) ) e. CC )
16 5 14 15 sylancr 
 |-  ( ( T. /\ x e. S ) -> ( 1 - ( _i x. x ) ) e. CC )
17 11 simp2d 
 |-  ( ( T. /\ x e. S ) -> ( 1 - ( _i x. x ) ) =/= 0 )
18 16 17 logcld 
 |-  ( ( T. /\ x e. S ) -> ( log ` ( 1 - ( _i x. x ) ) ) e. CC )
19 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 + ( _i x. x ) ) e. CC )
20 5 14 19 sylancr 
 |-  ( ( T. /\ x e. S ) -> ( 1 + ( _i x. x ) ) e. CC )
21 11 simp3d 
 |-  ( ( T. /\ x e. S ) -> ( 1 + ( _i x. x ) ) =/= 0 )
22 20 21 logcld 
 |-  ( ( T. /\ x e. S ) -> ( log ` ( 1 + ( _i x. x ) ) ) e. CC )
23 18 22 subcld 
 |-  ( ( T. /\ x e. S ) -> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) e. CC )
24 ovexd 
 |-  ( ( T. /\ x e. S ) -> ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) e. _V )
25 ovexd 
 |-  ( ( T. /\ x e. S ) -> ( 1 / ( x + _i ) ) e. _V )
26 1 2 atans2 
 |-  ( x e. S <-> ( x e. CC /\ ( 1 - ( _i x. x ) ) e. D /\ ( 1 + ( _i x. x ) ) e. D ) )
27 26 simp2bi 
 |-  ( x e. S -> ( 1 - ( _i x. x ) ) e. D )
28 27 adantl 
 |-  ( ( T. /\ x e. S ) -> ( 1 - ( _i x. x ) ) e. D )
29 negex 
 |-  -u _i e. _V
30 29 a1i 
 |-  ( ( T. /\ x e. S ) -> -u _i e. _V )
31 1 logdmss 
 |-  D C_ ( CC \ { 0 } )
32 simpr 
 |-  ( ( T. /\ y e. D ) -> y e. D )
33 31 32 sselid 
 |-  ( ( T. /\ y e. D ) -> y e. ( CC \ { 0 } ) )
34 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
35 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
36 34 35 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
37 36 ffvelcdmi 
 |-  ( y e. ( CC \ { 0 } ) -> ( log ` y ) e. ran log )
38 logrncn 
 |-  ( ( log ` y ) e. ran log -> ( log ` y ) e. CC )
39 33 37 38 3syl 
 |-  ( ( T. /\ y e. D ) -> ( log ` y ) e. CC )
40 ovexd 
 |-  ( ( T. /\ y e. D ) -> ( 1 / y ) e. _V )
41 6 a1i 
 |-  ( T. -> _i e. CC )
42 41 13 sylan 
 |-  ( ( T. /\ x e. CC ) -> ( _i x. x ) e. CC )
43 5 42 15 sylancr 
 |-  ( ( T. /\ x e. CC ) -> ( 1 - ( _i x. x ) ) e. CC )
44 29 a1i 
 |-  ( ( T. /\ x e. CC ) -> -u _i e. _V )
45 1cnd 
 |-  ( ( T. /\ x e. CC ) -> 1 e. CC )
46 0cnd 
 |-  ( ( T. /\ x e. CC ) -> 0 e. CC )
47 1cnd 
 |-  ( T. -> 1 e. CC )
48 4 47 dvmptc 
 |-  ( T. -> ( CC _D ( x e. CC |-> 1 ) ) = ( x e. CC |-> 0 ) )
49 6 a1i 
 |-  ( ( T. /\ x e. CC ) -> _i e. CC )
50 simpr 
 |-  ( ( T. /\ x e. CC ) -> x e. CC )
51 4 dvmptid 
 |-  ( T. -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
52 4 50 45 51 41 dvmptcmul 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = ( x e. CC |-> ( _i x. 1 ) ) )
53 6 mulridi 
 |-  ( _i x. 1 ) = _i
54 53 mpteq2i 
 |-  ( x e. CC |-> ( _i x. 1 ) ) = ( x e. CC |-> _i )
55 52 54 eqtrdi 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = ( x e. CC |-> _i ) )
56 4 45 46 48 42 49 55 dvmptsub 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 - ( _i x. x ) ) ) ) = ( x e. CC |-> ( 0 - _i ) ) )
57 df-neg 
 |-  -u _i = ( 0 - _i )
58 57 mpteq2i 
 |-  ( x e. CC |-> -u _i ) = ( x e. CC |-> ( 0 - _i ) )
59 56 58 eqtr4di 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 - ( _i x. x ) ) ) ) = ( x e. CC |-> -u _i ) )
60 2 ssrab3 
 |-  S C_ CC
61 60 a1i 
 |-  ( T. -> S C_ CC )
62 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
63 62 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
64 63 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
65 1 2 atansopn 
 |-  S e. ( TopOpen ` CCfld )
66 65 a1i 
 |-  ( T. -> S e. ( TopOpen ` CCfld ) )
67 4 43 44 59 61 64 62 66 dvmptres 
 |-  ( T. -> ( CC _D ( x e. S |-> ( 1 - ( _i x. x ) ) ) ) = ( x e. S |-> -u _i ) )
68 fssres 
 |-  ( ( log : ( CC \ { 0 } ) --> ran log /\ D C_ ( CC \ { 0 } ) ) -> ( log |` D ) : D --> ran log )
69 36 31 68 mp2an 
 |-  ( log |` D ) : D --> ran log
70 69 a1i 
 |-  ( T. -> ( log |` D ) : D --> ran log )
71 70 feqmptd 
 |-  ( T. -> ( log |` D ) = ( y e. D |-> ( ( log |` D ) ` y ) ) )
72 fvres 
 |-  ( y e. D -> ( ( log |` D ) ` y ) = ( log ` y ) )
73 72 mpteq2ia 
 |-  ( y e. D |-> ( ( log |` D ) ` y ) ) = ( y e. D |-> ( log ` y ) )
74 71 73 eqtr2di 
 |-  ( T. -> ( y e. D |-> ( log ` y ) ) = ( log |` D ) )
75 74 oveq2d 
 |-  ( T. -> ( CC _D ( y e. D |-> ( log ` y ) ) ) = ( CC _D ( log |` D ) ) )
76 1 dvlog 
 |-  ( CC _D ( log |` D ) ) = ( y e. D |-> ( 1 / y ) )
77 75 76 eqtrdi 
 |-  ( T. -> ( CC _D ( y e. D |-> ( log ` y ) ) ) = ( y e. D |-> ( 1 / y ) ) )
78 fveq2 
 |-  ( y = ( 1 - ( _i x. x ) ) -> ( log ` y ) = ( log ` ( 1 - ( _i x. x ) ) ) )
79 oveq2 
 |-  ( y = ( 1 - ( _i x. x ) ) -> ( 1 / y ) = ( 1 / ( 1 - ( _i x. x ) ) ) )
80 4 4 28 30 39 40 67 77 78 79 dvmptco 
 |-  ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 - ( _i x. x ) ) ) ) ) = ( x e. S |-> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i ) ) )
81 irec 
 |-  ( 1 / _i ) = -u _i
82 81 oveq2i 
 |-  ( ( 1 / ( 1 - ( _i x. x ) ) ) x. ( 1 / _i ) ) = ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i )
83 6 a1i 
 |-  ( ( T. /\ x e. S ) -> _i e. CC )
84 ine0 
 |-  _i =/= 0
85 84 a1i 
 |-  ( ( T. /\ x e. S ) -> _i =/= 0 )
86 16 83 17 85 recdiv2d 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) / _i ) = ( 1 / ( ( 1 - ( _i x. x ) ) x. _i ) ) )
87 16 17 reccld 
 |-  ( ( T. /\ x e. S ) -> ( 1 / ( 1 - ( _i x. x ) ) ) e. CC )
88 87 83 85 divrecd 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) / _i ) = ( ( 1 / ( 1 - ( _i x. x ) ) ) x. ( 1 / _i ) ) )
89 1cnd 
 |-  ( ( T. /\ x e. S ) -> 1 e. CC )
90 89 14 83 subdird 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 - ( _i x. x ) ) x. _i ) = ( ( 1 x. _i ) - ( ( _i x. x ) x. _i ) ) )
91 6 mullidi 
 |-  ( 1 x. _i ) = _i
92 91 a1i 
 |-  ( ( T. /\ x e. S ) -> ( 1 x. _i ) = _i )
93 83 12 83 mul32d 
 |-  ( ( T. /\ x e. S ) -> ( ( _i x. x ) x. _i ) = ( ( _i x. _i ) x. x ) )
94 ixi 
 |-  ( _i x. _i ) = -u 1
95 94 oveq1i 
 |-  ( ( _i x. _i ) x. x ) = ( -u 1 x. x )
96 12 mulm1d 
 |-  ( ( T. /\ x e. S ) -> ( -u 1 x. x ) = -u x )
97 95 96 eqtrid 
 |-  ( ( T. /\ x e. S ) -> ( ( _i x. _i ) x. x ) = -u x )
98 93 97 eqtrd 
 |-  ( ( T. /\ x e. S ) -> ( ( _i x. x ) x. _i ) = -u x )
99 92 98 oveq12d 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 x. _i ) - ( ( _i x. x ) x. _i ) ) = ( _i - -u x ) )
100 subneg 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i - -u x ) = ( _i + x ) )
101 6 12 100 sylancr 
 |-  ( ( T. /\ x e. S ) -> ( _i - -u x ) = ( _i + x ) )
102 90 99 101 3eqtrd 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 - ( _i x. x ) ) x. _i ) = ( _i + x ) )
103 83 12 102 comraddd 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 - ( _i x. x ) ) x. _i ) = ( x + _i ) )
104 103 oveq2d 
 |-  ( ( T. /\ x e. S ) -> ( 1 / ( ( 1 - ( _i x. x ) ) x. _i ) ) = ( 1 / ( x + _i ) ) )
105 86 88 104 3eqtr3d 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. ( 1 / _i ) ) = ( 1 / ( x + _i ) ) )
106 82 105 eqtr3id 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i ) = ( 1 / ( x + _i ) ) )
107 106 mpteq2dva 
 |-  ( T. -> ( x e. S |-> ( ( 1 / ( 1 - ( _i x. x ) ) ) x. -u _i ) ) = ( x e. S |-> ( 1 / ( x + _i ) ) ) )
108 80 107 eqtrd 
 |-  ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 - ( _i x. x ) ) ) ) ) = ( x e. S |-> ( 1 / ( x + _i ) ) ) )
109 ovexd 
 |-  ( ( T. /\ x e. S ) -> ( 1 / ( x - _i ) ) e. _V )
110 26 simp3bi 
 |-  ( x e. S -> ( 1 + ( _i x. x ) ) e. D )
111 110 adantl 
 |-  ( ( T. /\ x e. S ) -> ( 1 + ( _i x. x ) ) e. D )
112 5 42 19 sylancr 
 |-  ( ( T. /\ x e. CC ) -> ( 1 + ( _i x. x ) ) e. CC )
113 4 45 46 48 42 49 55 dvmptadd 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 + ( _i x. x ) ) ) ) = ( x e. CC |-> ( 0 + _i ) ) )
114 6 addlidi 
 |-  ( 0 + _i ) = _i
115 114 mpteq2i 
 |-  ( x e. CC |-> ( 0 + _i ) ) = ( x e. CC |-> _i )
116 113 115 eqtrdi 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 + ( _i x. x ) ) ) ) = ( x e. CC |-> _i ) )
117 4 112 49 116 61 64 62 66 dvmptres 
 |-  ( T. -> ( CC _D ( x e. S |-> ( 1 + ( _i x. x ) ) ) ) = ( x e. S |-> _i ) )
118 fveq2 
 |-  ( y = ( 1 + ( _i x. x ) ) -> ( log ` y ) = ( log ` ( 1 + ( _i x. x ) ) ) )
119 oveq2 
 |-  ( y = ( 1 + ( _i x. x ) ) -> ( 1 / y ) = ( 1 / ( 1 + ( _i x. x ) ) ) )
120 4 4 111 83 39 40 117 77 118 119 dvmptco 
 |-  ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 + ( _i x. x ) ) ) ) ) = ( x e. S |-> ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) ) )
121 89 20 83 21 85 divdiv2d 
 |-  ( ( T. /\ x e. S ) -> ( 1 / ( ( 1 + ( _i x. x ) ) / _i ) ) = ( ( 1 x. _i ) / ( 1 + ( _i x. x ) ) ) )
122 89 14 83 85 divdird 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 + ( _i x. x ) ) / _i ) = ( ( 1 / _i ) + ( ( _i x. x ) / _i ) ) )
123 81 a1i 
 |-  ( ( T. /\ x e. S ) -> ( 1 / _i ) = -u _i )
124 12 83 85 divcan3d 
 |-  ( ( T. /\ x e. S ) -> ( ( _i x. x ) / _i ) = x )
125 123 124 oveq12d 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 / _i ) + ( ( _i x. x ) / _i ) ) = ( -u _i + x ) )
126 negicn 
 |-  -u _i e. CC
127 addcom 
 |-  ( ( -u _i e. CC /\ x e. CC ) -> ( -u _i + x ) = ( x + -u _i ) )
128 126 12 127 sylancr 
 |-  ( ( T. /\ x e. S ) -> ( -u _i + x ) = ( x + -u _i ) )
129 negsub 
 |-  ( ( x e. CC /\ _i e. CC ) -> ( x + -u _i ) = ( x - _i ) )
130 12 6 129 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( x + -u _i ) = ( x - _i ) )
131 128 130 eqtrd 
 |-  ( ( T. /\ x e. S ) -> ( -u _i + x ) = ( x - _i ) )
132 122 125 131 3eqtrd 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 + ( _i x. x ) ) / _i ) = ( x - _i ) )
133 132 oveq2d 
 |-  ( ( T. /\ x e. S ) -> ( 1 / ( ( 1 + ( _i x. x ) ) / _i ) ) = ( 1 / ( x - _i ) ) )
134 89 83 20 21 div23d 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 x. _i ) / ( 1 + ( _i x. x ) ) ) = ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) )
135 121 133 134 3eqtr3rd 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) = ( 1 / ( x - _i ) ) )
136 135 mpteq2dva 
 |-  ( T. -> ( x e. S |-> ( ( 1 / ( 1 + ( _i x. x ) ) ) x. _i ) ) = ( x e. S |-> ( 1 / ( x - _i ) ) ) )
137 120 136 eqtrd 
 |-  ( T. -> ( CC _D ( x e. S |-> ( log ` ( 1 + ( _i x. x ) ) ) ) ) = ( x e. S |-> ( 1 / ( x - _i ) ) ) )
138 4 18 25 108 22 109 137 dvmptsub 
 |-  ( T. -> ( CC _D ( x e. S |-> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) = ( x e. S |-> ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) ) )
139 subcl 
 |-  ( ( x e. CC /\ _i e. CC ) -> ( x - _i ) e. CC )
140 12 6 139 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( x - _i ) e. CC )
141 addcl 
 |-  ( ( x e. CC /\ _i e. CC ) -> ( x + _i ) e. CC )
142 12 6 141 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( x + _i ) e. CC )
143 12 sqcld 
 |-  ( ( T. /\ x e. S ) -> ( x ^ 2 ) e. CC )
144 addcl 
 |-  ( ( 1 e. CC /\ ( x ^ 2 ) e. CC ) -> ( 1 + ( x ^ 2 ) ) e. CC )
145 5 143 144 sylancr 
 |-  ( ( T. /\ x e. S ) -> ( 1 + ( x ^ 2 ) ) e. CC )
146 atandm4 
 |-  ( x e. dom arctan <-> ( x e. CC /\ ( 1 + ( x ^ 2 ) ) =/= 0 ) )
147 146 simprbi 
 |-  ( x e. dom arctan -> ( 1 + ( x ^ 2 ) ) =/= 0 )
148 9 147 syl 
 |-  ( ( T. /\ x e. S ) -> ( 1 + ( x ^ 2 ) ) =/= 0 )
149 140 142 145 148 divsubdird 
 |-  ( ( T. /\ x e. S ) -> ( ( ( x - _i ) - ( x + _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) - ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
150 130 oveq1d 
 |-  ( ( T. /\ x e. S ) -> ( ( x + -u _i ) - ( x + _i ) ) = ( ( x - _i ) - ( x + _i ) ) )
151 126 a1i 
 |-  ( ( T. /\ x e. S ) -> -u _i e. CC )
152 12 151 83 pnpcand 
 |-  ( ( T. /\ x e. S ) -> ( ( x + -u _i ) - ( x + _i ) ) = ( -u _i - _i ) )
153 150 152 eqtr3d 
 |-  ( ( T. /\ x e. S ) -> ( ( x - _i ) - ( x + _i ) ) = ( -u _i - _i ) )
154 2cn 
 |-  2 e. CC
155 154 6 84 divreci 
 |-  ( 2 / _i ) = ( 2 x. ( 1 / _i ) )
156 81 oveq2i 
 |-  ( 2 x. ( 1 / _i ) ) = ( 2 x. -u _i )
157 155 156 eqtri 
 |-  ( 2 / _i ) = ( 2 x. -u _i )
158 126 2timesi 
 |-  ( 2 x. -u _i ) = ( -u _i + -u _i )
159 126 6 negsubi 
 |-  ( -u _i + -u _i ) = ( -u _i - _i )
160 157 158 159 3eqtri 
 |-  ( 2 / _i ) = ( -u _i - _i )
161 153 160 eqtr4di 
 |-  ( ( T. /\ x e. S ) -> ( ( x - _i ) - ( x + _i ) ) = ( 2 / _i ) )
162 161 oveq1d 
 |-  ( ( T. /\ x e. S ) -> ( ( ( x - _i ) - ( x + _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) )
163 140 mulridd 
 |-  ( ( T. /\ x e. S ) -> ( ( x - _i ) x. 1 ) = ( x - _i ) )
164 140 142 mulcomd 
 |-  ( ( T. /\ x e. S ) -> ( ( x - _i ) x. ( x + _i ) ) = ( ( x + _i ) x. ( x - _i ) ) )
165 i2 
 |-  ( _i ^ 2 ) = -u 1
166 165 oveq2i 
 |-  ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x ^ 2 ) - -u 1 )
167 subneg 
 |-  ( ( ( x ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( x ^ 2 ) - -u 1 ) = ( ( x ^ 2 ) + 1 ) )
168 143 5 167 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) - -u 1 ) = ( ( x ^ 2 ) + 1 ) )
169 166 168 eqtrid 
 |-  ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x ^ 2 ) + 1 ) )
170 subsq 
 |-  ( ( x e. CC /\ _i e. CC ) -> ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x + _i ) x. ( x - _i ) ) )
171 12 6 170 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) - ( _i ^ 2 ) ) = ( ( x + _i ) x. ( x - _i ) ) )
172 addcom 
 |-  ( ( ( x ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( x ^ 2 ) + 1 ) = ( 1 + ( x ^ 2 ) ) )
173 143 5 172 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( ( x ^ 2 ) + 1 ) = ( 1 + ( x ^ 2 ) ) )
174 169 171 173 3eqtr3d 
 |-  ( ( T. /\ x e. S ) -> ( ( x + _i ) x. ( x - _i ) ) = ( 1 + ( x ^ 2 ) ) )
175 164 174 eqtrd 
 |-  ( ( T. /\ x e. S ) -> ( ( x - _i ) x. ( x + _i ) ) = ( 1 + ( x ^ 2 ) ) )
176 163 175 oveq12d 
 |-  ( ( T. /\ x e. S ) -> ( ( ( x - _i ) x. 1 ) / ( ( x - _i ) x. ( x + _i ) ) ) = ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) )
177 subneg 
 |-  ( ( x e. CC /\ _i e. CC ) -> ( x - -u _i ) = ( x + _i ) )
178 12 6 177 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( x - -u _i ) = ( x + _i ) )
179 atandm 
 |-  ( x e. dom arctan <-> ( x e. CC /\ x =/= -u _i /\ x =/= _i ) )
180 9 179 sylib 
 |-  ( ( T. /\ x e. S ) -> ( x e. CC /\ x =/= -u _i /\ x =/= _i ) )
181 180 simp2d 
 |-  ( ( T. /\ x e. S ) -> x =/= -u _i )
182 subeq0 
 |-  ( ( x e. CC /\ -u _i e. CC ) -> ( ( x - -u _i ) = 0 <-> x = -u _i ) )
183 182 necon3bid 
 |-  ( ( x e. CC /\ -u _i e. CC ) -> ( ( x - -u _i ) =/= 0 <-> x =/= -u _i ) )
184 12 126 183 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( ( x - -u _i ) =/= 0 <-> x =/= -u _i ) )
185 181 184 mpbird 
 |-  ( ( T. /\ x e. S ) -> ( x - -u _i ) =/= 0 )
186 178 185 eqnetrrd 
 |-  ( ( T. /\ x e. S ) -> ( x + _i ) =/= 0 )
187 180 simp3d 
 |-  ( ( T. /\ x e. S ) -> x =/= _i )
188 subeq0 
 |-  ( ( x e. CC /\ _i e. CC ) -> ( ( x - _i ) = 0 <-> x = _i ) )
189 188 necon3bid 
 |-  ( ( x e. CC /\ _i e. CC ) -> ( ( x - _i ) =/= 0 <-> x =/= _i ) )
190 12 6 189 sylancl 
 |-  ( ( T. /\ x e. S ) -> ( ( x - _i ) =/= 0 <-> x =/= _i ) )
191 187 190 mpbird 
 |-  ( ( T. /\ x e. S ) -> ( x - _i ) =/= 0 )
192 89 142 140 186 191 divcan5d 
 |-  ( ( T. /\ x e. S ) -> ( ( ( x - _i ) x. 1 ) / ( ( x - _i ) x. ( x + _i ) ) ) = ( 1 / ( x + _i ) ) )
193 176 192 eqtr3d 
 |-  ( ( T. /\ x e. S ) -> ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) = ( 1 / ( x + _i ) ) )
194 142 mulridd 
 |-  ( ( T. /\ x e. S ) -> ( ( x + _i ) x. 1 ) = ( x + _i ) )
195 194 174 oveq12d 
 |-  ( ( T. /\ x e. S ) -> ( ( ( x + _i ) x. 1 ) / ( ( x + _i ) x. ( x - _i ) ) ) = ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) )
196 89 140 142 191 186 divcan5d 
 |-  ( ( T. /\ x e. S ) -> ( ( ( x + _i ) x. 1 ) / ( ( x + _i ) x. ( x - _i ) ) ) = ( 1 / ( x - _i ) ) )
197 195 196 eqtr3d 
 |-  ( ( T. /\ x e. S ) -> ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) = ( 1 / ( x - _i ) ) )
198 193 197 oveq12d 
 |-  ( ( T. /\ x e. S ) -> ( ( ( x - _i ) / ( 1 + ( x ^ 2 ) ) ) - ( ( x + _i ) / ( 1 + ( x ^ 2 ) ) ) ) = ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) )
199 149 162 198 3eqtr3rd 
 |-  ( ( T. /\ x e. S ) -> ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) = ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) )
200 199 mpteq2dva 
 |-  ( T. -> ( x e. S |-> ( ( 1 / ( x + _i ) ) - ( 1 / ( x - _i ) ) ) ) = ( x e. S |-> ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
201 138 200 eqtrd 
 |-  ( T. -> ( CC _D ( x e. S |-> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) = ( x e. S |-> ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
202 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
203 6 202 mp1i 
 |-  ( T. -> ( _i / 2 ) e. CC )
204 4 23 24 201 203 dvmptcmul 
 |-  ( T. -> ( CC _D ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) ) )
205 df-atan 
 |-  arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
206 205 reseq1i 
 |-  ( arctan |` S ) = ( ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) |` S )
207 atanf 
 |-  arctan : ( CC \ { -u _i , _i } ) --> CC
208 207 fdmi 
 |-  dom arctan = ( CC \ { -u _i , _i } )
209 7 208 sseqtri 
 |-  S C_ ( CC \ { -u _i , _i } )
210 resmpt 
 |-  ( S C_ ( CC \ { -u _i , _i } ) -> ( ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) )
211 209 210 ax-mp 
 |-  ( ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
212 206 211 eqtri 
 |-  ( arctan |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
213 212 a1i 
 |-  ( T. -> ( arctan |` S ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) )
214 213 oveq2d 
 |-  ( T. -> ( CC _D ( arctan |` S ) ) = ( CC _D ( x e. S |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) ) ) )
215 2ne0 
 |-  2 =/= 0
216 divcan6 
 |-  ( ( ( _i e. CC /\ _i =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( _i / 2 ) x. ( 2 / _i ) ) = 1 )
217 6 84 154 215 216 mp4an 
 |-  ( ( _i / 2 ) x. ( 2 / _i ) ) = 1
218 217 oveq1i 
 |-  ( ( ( _i / 2 ) x. ( 2 / _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( 1 / ( 1 + ( x ^ 2 ) ) )
219 6 202 mp1i 
 |-  ( ( T. /\ x e. S ) -> ( _i / 2 ) e. CC )
220 154 6 84 divcli 
 |-  ( 2 / _i ) e. CC
221 220 a1i 
 |-  ( ( T. /\ x e. S ) -> ( 2 / _i ) e. CC )
222 219 221 145 148 divassd 
 |-  ( ( T. /\ x e. S ) -> ( ( ( _i / 2 ) x. ( 2 / _i ) ) / ( 1 + ( x ^ 2 ) ) ) = ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
223 218 222 eqtr3id 
 |-  ( ( T. /\ x e. S ) -> ( 1 / ( 1 + ( x ^ 2 ) ) ) = ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) )
224 223 mpteq2dva 
 |-  ( T. -> ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) ) = ( x e. S |-> ( ( _i / 2 ) x. ( ( 2 / _i ) / ( 1 + ( x ^ 2 ) ) ) ) ) )
225 204 214 224 3eqtr4d 
 |-  ( T. -> ( CC _D ( arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) ) )
226 225 mptru 
 |-  ( CC _D ( arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) )