Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
|- _i e. CC |
2 |
|
atandm2 |
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) ) |
3 |
2
|
simp1bi |
|- ( A e. dom arctan -> A e. CC ) |
4 |
|
mulneg2 |
|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) ) |
5 |
1 3 4
|
sylancr |
|- ( A e. dom arctan -> ( _i x. -u A ) = -u ( _i x. A ) ) |
6 |
5
|
oveq2d |
|- ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 - -u ( _i x. A ) ) ) |
7 |
|
ax-1cn |
|- 1 e. CC |
8 |
|
mulcl |
|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC ) |
9 |
1 3 8
|
sylancr |
|- ( A e. dom arctan -> ( _i x. A ) e. CC ) |
10 |
|
subneg |
|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) ) |
11 |
7 9 10
|
sylancr |
|- ( A e. dom arctan -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) ) |
12 |
6 11
|
eqtrd |
|- ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 + ( _i x. A ) ) ) |
13 |
12
|
fveq2d |
|- ( A e. dom arctan -> ( log ` ( 1 - ( _i x. -u A ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) ) |
14 |
5
|
oveq2d |
|- ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 + -u ( _i x. A ) ) ) |
15 |
|
negsub |
|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) ) |
16 |
7 9 15
|
sylancr |
|- ( A e. dom arctan -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) ) |
17 |
14 16
|
eqtrd |
|- ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 - ( _i x. A ) ) ) |
18 |
17
|
fveq2d |
|- ( A e. dom arctan -> ( log ` ( 1 + ( _i x. -u A ) ) ) = ( log ` ( 1 - ( _i x. A ) ) ) ) |
19 |
13 18
|
oveq12d |
|- ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) |
20 |
|
subcl |
|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC ) |
21 |
7 9 20
|
sylancr |
|- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC ) |
22 |
2
|
simp2bi |
|- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 ) |
23 |
21 22
|
logcld |
|- ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC ) |
24 |
|
addcl |
|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC ) |
25 |
7 9 24
|
sylancr |
|- ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC ) |
26 |
2
|
simp3bi |
|- ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 ) |
27 |
25 26
|
logcld |
|- ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC ) |
28 |
23 27
|
negsubdi2d |
|- ( A e. dom arctan -> -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) |
29 |
19 28
|
eqtr4d |
|- ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) = -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) |
30 |
29
|
oveq2d |
|- ( A e. dom arctan -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) = ( ( _i / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) |
31 |
|
halfcl |
|- ( _i e. CC -> ( _i / 2 ) e. CC ) |
32 |
1 31
|
ax-mp |
|- ( _i / 2 ) e. CC |
33 |
23 27
|
subcld |
|- ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC ) |
34 |
|
mulneg2 |
|- ( ( ( _i / 2 ) e. CC /\ ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC ) -> ( ( _i / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) |
35 |
32 33 34
|
sylancr |
|- ( A e. dom arctan -> ( ( _i / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) |
36 |
30 35
|
eqtrd |
|- ( A e. dom arctan -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) |
37 |
|
atandmneg |
|- ( A e. dom arctan -> -u A e. dom arctan ) |
38 |
|
atanval |
|- ( -u A e. dom arctan -> ( arctan ` -u A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) ) |
39 |
37 38
|
syl |
|- ( A e. dom arctan -> ( arctan ` -u A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) ) |
40 |
|
atanval |
|- ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) |
41 |
40
|
negeqd |
|- ( A e. dom arctan -> -u ( arctan ` A ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) |
42 |
36 39 41
|
3eqtr4d |
|- ( A e. dom arctan -> ( arctan ` -u A ) = -u ( arctan ` A ) ) |