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 ffvelrni
 |-  ( 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 mulid1i
 |-  ( _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 mulid2i
 |-  ( 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 syl5eq
 |-  ( ( 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 addid2i
 |-  ( 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 mulid1d
 |-  ( ( 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 syl5eq
 |-  ( ( 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 mulid1d
 |-  ( ( 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 ) ) ) )