Metamath Proof Explorer

Theorem atancj

Description: The arctangent function distributes under conjugation. (The condition that Re ( A ) =/= 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -u 1 and 1 , though.) (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atancj 
|- ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A e. dom arctan /\ ( * ` ( arctan ` A ) ) = ( arctan ` ( * ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> A e. CC )
2 simpr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) =/= 0 )
3 fveq2 
 |-  ( A = -u _i -> ( Re ` A ) = ( Re ` -u _i ) )
4 ax-icn 
 |-  _i e. CC
5 4 renegi 
 |-  ( Re ` -u _i ) = -u ( Re ` _i )
6 rei 
 |-  ( Re ` _i ) = 0
7 6 negeqi 
 |-  -u ( Re ` _i ) = -u 0
8 neg0 
 |-  -u 0 = 0
9 5 7 8 3eqtri 
 |-  ( Re ` -u _i ) = 0
10 3 9 eqtrdi 
 |-  ( A = -u _i -> ( Re ` A ) = 0 )
11 10 necon3i 
 |-  ( ( Re ` A ) =/= 0 -> A =/= -u _i )
12 2 11 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> A =/= -u _i )
13 fveq2 
 |-  ( A = _i -> ( Re ` A ) = ( Re ` _i ) )
14 13 6 eqtrdi 
 |-  ( A = _i -> ( Re ` A ) = 0 )
15 14 necon3i 
 |-  ( ( Re ` A ) =/= 0 -> A =/= _i )
16 2 15 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> A =/= _i )
17 atandm 
 |-  ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
18 1 12 16 17 syl3anbrc 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> A e. dom arctan )
19 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
20 4 19 ax-mp 
 |-  ( _i / 2 ) e. CC
21 ax-1cn 
 |-  1 e. CC
22 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
23 4 1 22 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. A ) e. CC )
24 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
25 21 23 24 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 - ( _i x. A ) ) e. CC )
26 atandm2 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
27 18 26 sylib 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
28 27 simp2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 - ( _i x. A ) ) =/= 0 )
29 25 28 logcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
30 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
31 21 23 30 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 + ( _i x. A ) ) e. CC )
32 27 simp3d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 + ( _i x. A ) ) =/= 0 )
33 31 32 logcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
34 29 33 subcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
35 cjmul 
 |-  ( ( ( _i / 2 ) e. CC /\ ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC ) -> ( * ` ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( * ` ( _i / 2 ) ) x. ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
36 20 34 35 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( * ` ( _i / 2 ) ) x. ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
37 2ne0 
 |-  2 =/= 0
38 2cn 
 |-  2 e. CC
39 4 38 cjdivi 
 |-  ( 2 =/= 0 -> ( * ` ( _i / 2 ) ) = ( ( * ` _i ) / ( * ` 2 ) ) )
40 37 39 ax-mp 
 |-  ( * ` ( _i / 2 ) ) = ( ( * ` _i ) / ( * ` 2 ) )
41 divneg 
 |-  ( ( _i e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( _i / 2 ) = ( -u _i / 2 ) )
42 4 38 37 41 mp3an 
 |-  -u ( _i / 2 ) = ( -u _i / 2 )
43 cji 
 |-  ( * ` _i ) = -u _i
44 2re 
 |-  2 e. RR
45 cjre 
 |-  ( 2 e. RR -> ( * ` 2 ) = 2 )
46 44 45 ax-mp 
 |-  ( * ` 2 ) = 2
47 43 46 oveq12i 
 |-  ( ( * ` _i ) / ( * ` 2 ) ) = ( -u _i / 2 )
48 42 47 eqtr4i 
 |-  -u ( _i / 2 ) = ( ( * ` _i ) / ( * ` 2 ) )
49 40 48 eqtr4i 
 |-  ( * ` ( _i / 2 ) ) = -u ( _i / 2 )
50 49 oveq1i 
 |-  ( ( * ` ( _i / 2 ) ) x. ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( -u ( _i / 2 ) x. ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
51 34 cjcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) e. CC )
52 mulneg12 
 |-  ( ( ( _i / 2 ) e. CC /\ ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) e. CC ) -> ( -u ( _i / 2 ) x. ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( _i / 2 ) x. -u ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
53 20 51 52 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( -u ( _i / 2 ) x. ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( _i / 2 ) x. -u ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
54 50 53 syl5eq 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( * ` ( _i / 2 ) ) x. ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( _i / 2 ) x. -u ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
55 cjsub 
 |-  ( ( ( log ` ( 1 - ( _i x. A ) ) ) e. CC /\ ( log ` ( 1 + ( _i x. A ) ) ) e. CC ) -> ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( * ` ( log ` ( 1 - ( _i x. A ) ) ) ) - ( * ` ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
56 29 33 55 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( * ` ( log ` ( 1 - ( _i x. A ) ) ) ) - ( * ` ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
57 imsub 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( Im ` ( 1 - ( _i x. A ) ) ) = ( ( Im ` 1 ) - ( Im ` ( _i x. A ) ) ) )
58 21 23 57 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( 1 - ( _i x. A ) ) ) = ( ( Im ` 1 ) - ( Im ` ( _i x. A ) ) ) )
59 reim 
 |-  ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
60 59 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
61 60 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Im ` 1 ) - ( Re ` A ) ) = ( ( Im ` 1 ) - ( Im ` ( _i x. A ) ) ) )
62 58 61 eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( 1 - ( _i x. A ) ) ) = ( ( Im ` 1 ) - ( Re ` A ) ) )
63 df-neg 
 |-  -u ( Re ` A ) = ( 0 - ( Re ` A ) )
64 im1 
 |-  ( Im ` 1 ) = 0
65 64 oveq1i 
 |-  ( ( Im ` 1 ) - ( Re ` A ) ) = ( 0 - ( Re ` A ) )
66 63 65 eqtr4i 
 |-  -u ( Re ` A ) = ( ( Im ` 1 ) - ( Re ` A ) )
67 62 66 eqtr4di 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( 1 - ( _i x. A ) ) ) = -u ( Re ` A ) )
68 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
69 68 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) e. RR )
70 69 recnd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) e. CC )
71 70 2 negne0d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> -u ( Re ` A ) =/= 0 )
72 67 71 eqnetrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( 1 - ( _i x. A ) ) ) =/= 0 )
73 logcj 
 |-  ( ( ( 1 - ( _i x. A ) ) e. CC /\ ( Im ` ( 1 - ( _i x. A ) ) ) =/= 0 ) -> ( log ` ( * ` ( 1 - ( _i x. A ) ) ) ) = ( * ` ( log ` ( 1 - ( _i x. A ) ) ) ) )
74 25 72 73 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( * ` ( 1 - ( _i x. A ) ) ) ) = ( * ` ( log ` ( 1 - ( _i x. A ) ) ) ) )
75 cjsub 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( * ` ( 1 - ( _i x. A ) ) ) = ( ( * ` 1 ) - ( * ` ( _i x. A ) ) ) )
76 21 23 75 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( 1 - ( _i x. A ) ) ) = ( ( * ` 1 ) - ( * ` ( _i x. A ) ) ) )
77 1re 
 |-  1 e. RR
78 cjre 
 |-  ( 1 e. RR -> ( * ` 1 ) = 1 )
79 77 78 mp1i 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` 1 ) = 1 )
80 cjmul 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( * ` ( _i x. A ) ) = ( ( * ` _i ) x. ( * ` A ) ) )
81 4 1 80 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( _i x. A ) ) = ( ( * ` _i ) x. ( * ` A ) ) )
82 43 oveq1i 
 |-  ( ( * ` _i ) x. ( * ` A ) ) = ( -u _i x. ( * ` A ) )
83 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
84 83 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` A ) e. CC )
85 mulneg1 
 |-  ( ( _i e. CC /\ ( * ` A ) e. CC ) -> ( -u _i x. ( * ` A ) ) = -u ( _i x. ( * ` A ) ) )
86 4 84 85 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( -u _i x. ( * ` A ) ) = -u ( _i x. ( * ` A ) ) )
87 82 86 syl5eq 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( * ` _i ) x. ( * ` A ) ) = -u ( _i x. ( * ` A ) ) )
88 81 87 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( _i x. A ) ) = -u ( _i x. ( * ` A ) ) )
89 79 88 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( * ` 1 ) - ( * ` ( _i x. A ) ) ) = ( 1 - -u ( _i x. ( * ` A ) ) ) )
90 mulcl 
 |-  ( ( _i e. CC /\ ( * ` A ) e. CC ) -> ( _i x. ( * ` A ) ) e. CC )
91 4 84 90 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( * ` A ) ) e. CC )
92 subneg 
 |-  ( ( 1 e. CC /\ ( _i x. ( * ` A ) ) e. CC ) -> ( 1 - -u ( _i x. ( * ` A ) ) ) = ( 1 + ( _i x. ( * ` A ) ) ) )
93 21 91 92 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 - -u ( _i x. ( * ` A ) ) ) = ( 1 + ( _i x. ( * ` A ) ) ) )
94 76 89 93 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( 1 - ( _i x. A ) ) ) = ( 1 + ( _i x. ( * ` A ) ) ) )
95 94 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( * ` ( 1 - ( _i x. A ) ) ) ) = ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) )
96 74 95 eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( log ` ( 1 - ( _i x. A ) ) ) ) = ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) )
97 imadd 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( Im ` ( 1 + ( _i x. A ) ) ) = ( ( Im ` 1 ) + ( Im ` ( _i x. A ) ) ) )
98 21 23 97 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( 1 + ( _i x. A ) ) ) = ( ( Im ` 1 ) + ( Im ` ( _i x. A ) ) ) )
99 60 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 0 + ( Re ` A ) ) = ( 0 + ( Im ` ( _i x. A ) ) ) )
100 64 oveq1i 
 |-  ( ( Im ` 1 ) + ( Im ` ( _i x. A ) ) ) = ( 0 + ( Im ` ( _i x. A ) ) )
101 99 100 eqtr4di 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 0 + ( Re ` A ) ) = ( ( Im ` 1 ) + ( Im ` ( _i x. A ) ) ) )
102 70 addid2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 0 + ( Re ` A ) ) = ( Re ` A ) )
103 98 101 102 3eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( 1 + ( _i x. A ) ) ) = ( Re ` A ) )
104 103 2 eqnetrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( 1 + ( _i x. A ) ) ) =/= 0 )
105 logcj 
 |-  ( ( ( 1 + ( _i x. A ) ) e. CC /\ ( Im ` ( 1 + ( _i x. A ) ) ) =/= 0 ) -> ( log ` ( * ` ( 1 + ( _i x. A ) ) ) ) = ( * ` ( log ` ( 1 + ( _i x. A ) ) ) ) )
106 31 104 105 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( * ` ( 1 + ( _i x. A ) ) ) ) = ( * ` ( log ` ( 1 + ( _i x. A ) ) ) ) )
107 cjadd 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( * ` ( 1 + ( _i x. A ) ) ) = ( ( * ` 1 ) + ( * ` ( _i x. A ) ) ) )
108 21 23 107 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( 1 + ( _i x. A ) ) ) = ( ( * ` 1 ) + ( * ` ( _i x. A ) ) ) )
109 79 88 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( * ` 1 ) + ( * ` ( _i x. A ) ) ) = ( 1 + -u ( _i x. ( * ` A ) ) ) )
110 negsub 
 |-  ( ( 1 e. CC /\ ( _i x. ( * ` A ) ) e. CC ) -> ( 1 + -u ( _i x. ( * ` A ) ) ) = ( 1 - ( _i x. ( * ` A ) ) ) )
111 21 91 110 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 + -u ( _i x. ( * ` A ) ) ) = ( 1 - ( _i x. ( * ` A ) ) ) )
112 108 109 111 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( 1 + ( _i x. A ) ) ) = ( 1 - ( _i x. ( * ` A ) ) ) )
113 112 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( * ` ( 1 + ( _i x. A ) ) ) ) = ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) )
114 106 113 eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( log ` ( 1 + ( _i x. A ) ) ) ) = ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) )
115 96 114 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( * ` ( log ` ( 1 - ( _i x. A ) ) ) ) - ( * ` ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) ) )
116 56 115 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) ) )
117 116 negeqd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> -u ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = -u ( ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) ) )
118 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. ( * ` A ) ) e. CC ) -> ( 1 + ( _i x. ( * ` A ) ) ) e. CC )
119 21 91 118 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 + ( _i x. ( * ` A ) ) ) e. CC )
120 atandmcj 
 |-  ( A e. dom arctan -> ( * ` A ) e. dom arctan )
121 18 120 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` A ) e. dom arctan )
122 atandm2 
 |-  ( ( * ` A ) e. dom arctan <-> ( ( * ` A ) e. CC /\ ( 1 - ( _i x. ( * ` A ) ) ) =/= 0 /\ ( 1 + ( _i x. ( * ` A ) ) ) =/= 0 ) )
123 122 simp3bi 
 |-  ( ( * ` A ) e. dom arctan -> ( 1 + ( _i x. ( * ` A ) ) ) =/= 0 )
124 121 123 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 + ( _i x. ( * ` A ) ) ) =/= 0 )
125 119 124 logcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) e. CC )
126 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. ( * ` A ) ) e. CC ) -> ( 1 - ( _i x. ( * ` A ) ) ) e. CC )
127 21 91 126 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 - ( _i x. ( * ` A ) ) ) e. CC )
128 122 simp2bi 
 |-  ( ( * ` A ) e. dom arctan -> ( 1 - ( _i x. ( * ` A ) ) ) =/= 0 )
129 121 128 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 1 - ( _i x. ( * ` A ) ) ) =/= 0 )
130 127 129 logcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) e. CC )
131 125 130 negsubdi2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> -u ( ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) ) = ( ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) ) )
132 117 131 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> -u ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) ) )
133 132 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i / 2 ) x. -u ( * ` ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) ) ) )
134 36 54 133 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) ) ) )
135 atanval 
 |-  ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
136 18 135 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
137 136 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( arctan ` A ) ) = ( * ` ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
138 atanval 
 |-  ( ( * ` A ) e. dom arctan -> ( arctan ` ( * ` A ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) ) ) )
139 121 138 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( arctan ` ( * ` A ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( * ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( * ` A ) ) ) ) ) ) )
140 134 137 139 3eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( * ` ( arctan ` A ) ) = ( arctan ` ( * ` A ) ) )
141 18 140 jca 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A e. dom arctan /\ ( * ` ( arctan ` A ) ) = ( arctan ` ( * ` A ) ) ) )