Metamath Proof Explorer

Theorem atanlogsublem

Description: Lemma for atanlogsub . (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion atanlogsublem 
|- ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 ax-icn 
 |-  _i e. CC
3 simpl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> A e. dom arctan )
4 atandm2 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
5 3 4 sylib 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
6 5 simp1d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> A e. CC )
7 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
8 2 6 7 sylancr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. A ) e. CC )
9 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
10 1 8 9 sylancr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 1 + ( _i x. A ) ) e. CC )
11 5 simp3d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 1 + ( _i x. A ) ) =/= 0 )
12 10 11 logcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
13 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
14 1 8 13 sylancr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 1 - ( _i x. A ) ) e. CC )
15 5 simp2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 1 - ( _i x. A ) ) =/= 0 )
16 14 15 logcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
17 12 16 imsubd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) - ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
18 2 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> _i e. CC )
19 18 6 18 subdid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. ( A - _i ) ) = ( ( _i x. A ) - ( _i x. _i ) ) )
20 ixi 
 |-  ( _i x. _i ) = -u 1
21 20 oveq2i 
 |-  ( ( _i x. A ) - ( _i x. _i ) ) = ( ( _i x. A ) - -u 1 )
22 subneg 
 |-  ( ( ( _i x. A ) e. CC /\ 1 e. CC ) -> ( ( _i x. A ) - -u 1 ) = ( ( _i x. A ) + 1 ) )
23 8 1 22 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( _i x. A ) - -u 1 ) = ( ( _i x. A ) + 1 ) )
24 21 23 eqtrid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( _i x. A ) - ( _i x. _i ) ) = ( ( _i x. A ) + 1 ) )
25 addcom 
 |-  ( ( ( _i x. A ) e. CC /\ 1 e. CC ) -> ( ( _i x. A ) + 1 ) = ( 1 + ( _i x. A ) ) )
26 8 1 25 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( _i x. A ) + 1 ) = ( 1 + ( _i x. A ) ) )
27 19 24 26 3eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. ( A - _i ) ) = ( 1 + ( _i x. A ) ) )
28 27 fveq2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( _i x. ( A - _i ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
29 subcl 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( A - _i ) e. CC )
30 6 2 29 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( A - _i ) e. CC )
31 resub 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( Re ` ( A - _i ) ) = ( ( Re ` A ) - ( Re ` _i ) ) )
32 6 2 31 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` ( A - _i ) ) = ( ( Re ` A ) - ( Re ` _i ) ) )
33 rei 
 |-  ( Re ` _i ) = 0
34 33 oveq2i 
 |-  ( ( Re ` A ) - ( Re ` _i ) ) = ( ( Re ` A ) - 0 )
35 6 recld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` A ) e. RR )
36 35 recnd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` A ) e. CC )
37 36 subid1d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Re ` A ) - 0 ) = ( Re ` A ) )
38 34 37 eqtrid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Re ` A ) - ( Re ` _i ) ) = ( Re ` A ) )
39 32 38 eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` ( A - _i ) ) = ( Re ` A ) )
40 gt0ne0 
 |-  ( ( ( Re ` A ) e. RR /\ 0 < ( Re ` A ) ) -> ( Re ` A ) =/= 0 )
41 35 40 sylancom 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` A ) =/= 0 )
42 39 41 eqnetrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` ( A - _i ) ) =/= 0 )
43 fveq2 
 |-  ( ( A - _i ) = 0 -> ( Re ` ( A - _i ) ) = ( Re ` 0 ) )
44 re0 
 |-  ( Re ` 0 ) = 0
45 43 44 eqtrdi 
 |-  ( ( A - _i ) = 0 -> ( Re ` ( A - _i ) ) = 0 )
46 45 necon3i 
 |-  ( ( Re ` ( A - _i ) ) =/= 0 -> ( A - _i ) =/= 0 )
47 42 46 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( A - _i ) =/= 0 )
48 simpr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` A ) )
49 0re 
 |-  0 e. RR
50 ltle 
 |-  ( ( 0 e. RR /\ ( Re ` A ) e. RR ) -> ( 0 < ( Re ` A ) -> 0 <_ ( Re ` A ) ) )
51 49 35 50 sylancr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 0 < ( Re ` A ) -> 0 <_ ( Re ` A ) ) )
52 48 51 mpd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 <_ ( Re ` A ) )
53 52 39 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 <_ ( Re ` ( A - _i ) ) )
54 logimul 
 |-  ( ( ( A - _i ) e. CC /\ ( A - _i ) =/= 0 /\ 0 <_ ( Re ` ( A - _i ) ) ) -> ( log ` ( _i x. ( A - _i ) ) ) = ( ( log ` ( A - _i ) ) + ( _i x. ( _pi / 2 ) ) ) )
55 30 47 53 54 syl3anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( _i x. ( A - _i ) ) ) = ( ( log ` ( A - _i ) ) + ( _i x. ( _pi / 2 ) ) ) )
56 28 55 eqtr3d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( 1 + ( _i x. A ) ) ) = ( ( log ` ( A - _i ) ) + ( _i x. ( _pi / 2 ) ) ) )
57 56 fveq2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) = ( Im ` ( ( log ` ( A - _i ) ) + ( _i x. ( _pi / 2 ) ) ) ) )
58 30 47 logcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( A - _i ) ) e. CC )
59 halfpire 
 |-  ( _pi / 2 ) e. RR
60 59 recni 
 |-  ( _pi / 2 ) e. CC
61 2 60 mulcli 
 |-  ( _i x. ( _pi / 2 ) ) e. CC
62 imadd 
 |-  ( ( ( log ` ( A - _i ) ) e. CC /\ ( _i x. ( _pi / 2 ) ) e. CC ) -> ( Im ` ( ( log ` ( A - _i ) ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` ( A - _i ) ) ) + ( Im ` ( _i x. ( _pi / 2 ) ) ) ) )
63 58 61 62 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( A - _i ) ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` ( A - _i ) ) ) + ( Im ` ( _i x. ( _pi / 2 ) ) ) ) )
64 reim 
 |-  ( ( _pi / 2 ) e. CC -> ( Re ` ( _pi / 2 ) ) = ( Im ` ( _i x. ( _pi / 2 ) ) ) )
65 60 64 ax-mp 
 |-  ( Re ` ( _pi / 2 ) ) = ( Im ` ( _i x. ( _pi / 2 ) ) )
66 rere 
 |-  ( ( _pi / 2 ) e. RR -> ( Re ` ( _pi / 2 ) ) = ( _pi / 2 ) )
67 59 66 ax-mp 
 |-  ( Re ` ( _pi / 2 ) ) = ( _pi / 2 )
68 65 67 eqtr3i 
 |-  ( Im ` ( _i x. ( _pi / 2 ) ) ) = ( _pi / 2 )
69 68 oveq2i 
 |-  ( ( Im ` ( log ` ( A - _i ) ) ) + ( Im ` ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` ( A - _i ) ) ) + ( _pi / 2 ) )
70 63 69 eqtrdi 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( A - _i ) ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` ( A - _i ) ) ) + ( _pi / 2 ) ) )
71 57 70 eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) = ( ( Im ` ( log ` ( A - _i ) ) ) + ( _pi / 2 ) ) )
72 addcl 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( A + _i ) e. CC )
73 6 2 72 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( A + _i ) e. CC )
74 mulcl 
 |-  ( ( _i e. CC /\ ( A + _i ) e. CC ) -> ( _i x. ( A + _i ) ) e. CC )
75 2 73 74 sylancr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. ( A + _i ) ) e. CC )
76 reim 
 |-  ( ( A + _i ) e. CC -> ( Re ` ( A + _i ) ) = ( Im ` ( _i x. ( A + _i ) ) ) )
77 73 76 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` ( A + _i ) ) = ( Im ` ( _i x. ( A + _i ) ) ) )
78 readd 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( Re ` ( A + _i ) ) = ( ( Re ` A ) + ( Re ` _i ) ) )
79 6 2 78 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` ( A + _i ) ) = ( ( Re ` A ) + ( Re ` _i ) ) )
80 33 oveq2i 
 |-  ( ( Re ` A ) + ( Re ` _i ) ) = ( ( Re ` A ) + 0 )
81 36 addid1d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Re ` A ) + 0 ) = ( Re ` A ) )
82 80 81 eqtrid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Re ` A ) + ( Re ` _i ) ) = ( Re ` A ) )
83 79 82 eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` ( A + _i ) ) = ( Re ` A ) )
84 77 83 eqtr3d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( _i x. ( A + _i ) ) ) = ( Re ` A ) )
85 48 84 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 < ( Im ` ( _i x. ( A + _i ) ) ) )
86 logneg2 
 |-  ( ( ( _i x. ( A + _i ) ) e. CC /\ 0 < ( Im ` ( _i x. ( A + _i ) ) ) ) -> ( log ` -u ( _i x. ( A + _i ) ) ) = ( ( log ` ( _i x. ( A + _i ) ) ) - ( _i x. _pi ) ) )
87 75 85 86 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` -u ( _i x. ( A + _i ) ) ) = ( ( log ` ( _i x. ( A + _i ) ) ) - ( _i x. _pi ) ) )
88 18 6 18 adddid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. ( A + _i ) ) = ( ( _i x. A ) + ( _i x. _i ) ) )
89 20 oveq2i 
 |-  ( ( _i x. A ) + ( _i x. _i ) ) = ( ( _i x. A ) + -u 1 )
90 negsub 
 |-  ( ( ( _i x. A ) e. CC /\ 1 e. CC ) -> ( ( _i x. A ) + -u 1 ) = ( ( _i x. A ) - 1 ) )
91 8 1 90 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( _i x. A ) + -u 1 ) = ( ( _i x. A ) - 1 ) )
92 89 91 eqtrid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( _i x. A ) + ( _i x. _i ) ) = ( ( _i x. A ) - 1 ) )
93 88 92 eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. ( A + _i ) ) = ( ( _i x. A ) - 1 ) )
94 93 negeqd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u ( _i x. ( A + _i ) ) = -u ( ( _i x. A ) - 1 ) )
95 negsubdi2 
 |-  ( ( ( _i x. A ) e. CC /\ 1 e. CC ) -> -u ( ( _i x. A ) - 1 ) = ( 1 - ( _i x. A ) ) )
96 8 1 95 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u ( ( _i x. A ) - 1 ) = ( 1 - ( _i x. A ) ) )
97 94 96 eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u ( _i x. ( A + _i ) ) = ( 1 - ( _i x. A ) ) )
98 97 fveq2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` -u ( _i x. ( A + _i ) ) ) = ( log ` ( 1 - ( _i x. A ) ) ) )
99 83 41 eqnetrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` ( A + _i ) ) =/= 0 )
100 fveq2 
 |-  ( ( A + _i ) = 0 -> ( Re ` ( A + _i ) ) = ( Re ` 0 ) )
101 100 44 eqtrdi 
 |-  ( ( A + _i ) = 0 -> ( Re ` ( A + _i ) ) = 0 )
102 101 necon3i 
 |-  ( ( Re ` ( A + _i ) ) =/= 0 -> ( A + _i ) =/= 0 )
103 99 102 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( A + _i ) =/= 0 )
104 73 103 logcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( A + _i ) ) e. CC )
105 61 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. ( _pi / 2 ) ) e. CC )
106 picn 
 |-  _pi e. CC
107 2 106 mulcli 
 |-  ( _i x. _pi ) e. CC
108 107 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. _pi ) e. CC )
109 52 83 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 <_ ( Re ` ( A + _i ) ) )
110 logimul 
 |-  ( ( ( A + _i ) e. CC /\ ( A + _i ) =/= 0 /\ 0 <_ ( Re ` ( A + _i ) ) ) -> ( log ` ( _i x. ( A + _i ) ) ) = ( ( log ` ( A + _i ) ) + ( _i x. ( _pi / 2 ) ) ) )
111 73 103 109 110 syl3anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( _i x. ( A + _i ) ) ) = ( ( log ` ( A + _i ) ) + ( _i x. ( _pi / 2 ) ) ) )
112 111 oveq1d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( log ` ( _i x. ( A + _i ) ) ) - ( _i x. _pi ) ) = ( ( ( log ` ( A + _i ) ) + ( _i x. ( _pi / 2 ) ) ) - ( _i x. _pi ) ) )
113 104 105 108 112 assraddsubd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( log ` ( _i x. ( A + _i ) ) ) - ( _i x. _pi ) ) = ( ( log ` ( A + _i ) ) + ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) )
114 87 98 113 3eqtr3d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( 1 - ( _i x. A ) ) ) = ( ( log ` ( A + _i ) ) + ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) )
115 114 fveq2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) = ( Im ` ( ( log ` ( A + _i ) ) + ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) ) )
116 61 107 subcli 
 |-  ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) e. CC
117 imadd 
 |-  ( ( ( log ` ( A + _i ) ) e. CC /\ ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) e. CC ) -> ( Im ` ( ( log ` ( A + _i ) ) + ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) ) = ( ( Im ` ( log ` ( A + _i ) ) ) + ( Im ` ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) ) )
118 104 116 117 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( A + _i ) ) + ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) ) = ( ( Im ` ( log ` ( A + _i ) ) ) + ( Im ` ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) ) )
119 imsub 
 |-  ( ( ( _i x. ( _pi / 2 ) ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( Im ` ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) = ( ( Im ` ( _i x. ( _pi / 2 ) ) ) - ( Im ` ( _i x. _pi ) ) ) )
120 61 107 119 mp2an 
 |-  ( Im ` ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) = ( ( Im ` ( _i x. ( _pi / 2 ) ) ) - ( Im ` ( _i x. _pi ) ) )
121 reim 
 |-  ( _pi e. CC -> ( Re ` _pi ) = ( Im ` ( _i x. _pi ) ) )
122 106 121 ax-mp 
 |-  ( Re ` _pi ) = ( Im ` ( _i x. _pi ) )
123 pire 
 |-  _pi e. RR
124 rere 
 |-  ( _pi e. RR -> ( Re ` _pi ) = _pi )
125 123 124 ax-mp 
 |-  ( Re ` _pi ) = _pi
126 122 125 eqtr3i 
 |-  ( Im ` ( _i x. _pi ) ) = _pi
127 68 126 oveq12i 
 |-  ( ( Im ` ( _i x. ( _pi / 2 ) ) ) - ( Im ` ( _i x. _pi ) ) ) = ( ( _pi / 2 ) - _pi )
128 60 negcli 
 |-  -u ( _pi / 2 ) e. CC
129 106 60 negsubi 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi - ( _pi / 2 ) )
130 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
131 106 60 60 130 subaddrii 
 |-  ( _pi - ( _pi / 2 ) ) = ( _pi / 2 )
132 129 131 eqtri 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi / 2 )
133 60 106 128 132 subaddrii 
 |-  ( ( _pi / 2 ) - _pi ) = -u ( _pi / 2 )
134 120 127 133 3eqtri 
 |-  ( Im ` ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) = -u ( _pi / 2 )
135 134 oveq2i 
 |-  ( ( Im ` ( log ` ( A + _i ) ) ) + ( Im ` ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) ) = ( ( Im ` ( log ` ( A + _i ) ) ) + -u ( _pi / 2 ) )
136 118 135 eqtrdi 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( A + _i ) ) + ( ( _i x. ( _pi / 2 ) ) - ( _i x. _pi ) ) ) ) = ( ( Im ` ( log ` ( A + _i ) ) ) + -u ( _pi / 2 ) ) )
137 115 136 eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( Im ` ( log ` ( A + _i ) ) ) + -u ( _pi / 2 ) ) )
138 71 137 oveq12d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) - ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( ( Im ` ( log ` ( A - _i ) ) ) + ( _pi / 2 ) ) - ( ( Im ` ( log ` ( A + _i ) ) ) + -u ( _pi / 2 ) ) ) )
139 58 imcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A - _i ) ) ) e. RR )
140 139 recnd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A - _i ) ) ) e. CC )
141 60 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _pi / 2 ) e. CC )
142 104 imcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A + _i ) ) ) e. RR )
143 142 recnd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A + _i ) ) ) e. CC )
144 128 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u ( _pi / 2 ) e. CC )
145 140 141 143 144 addsub4d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) + ( _pi / 2 ) ) - ( ( Im ` ( log ` ( A + _i ) ) ) + -u ( _pi / 2 ) ) ) = ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) )
146 60 60 subnegi 
 |-  ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = ( ( _pi / 2 ) + ( _pi / 2 ) )
147 146 130 eqtri 
 |-  ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = _pi
148 147 oveq2i 
 |-  ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) = ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi )
149 145 148 eqtrdi 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) + ( _pi / 2 ) ) - ( ( Im ` ( log ` ( A + _i ) ) ) + -u ( _pi / 2 ) ) ) = ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) )
150 17 138 149 3eqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) )
151 139 142 resubcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) e. RR )
152 readdcl 
 |-  ( ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) e. RR /\ _pi e. RR ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) e. RR )
153 151 123 152 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) e. RR )
154 123 renegcli 
 |-  -u _pi e. RR
155 154 recni 
 |-  -u _pi e. CC
156 155 106 negsubi 
 |-  ( -u _pi + -u _pi ) = ( -u _pi - _pi )
157 154 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi e. RR )
158 142 renegcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u ( Im ` ( log ` ( A + _i ) ) ) e. RR )
159 30 47 logimcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( -u _pi < ( Im ` ( log ` ( A - _i ) ) ) /\ ( Im ` ( log ` ( A - _i ) ) ) <_ _pi ) )
160 159 simpld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi < ( Im ` ( log ` ( A - _i ) ) ) )
161 73 103 logimcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( -u _pi < ( Im ` ( log ` ( A + _i ) ) ) /\ ( Im ` ( log ` ( A + _i ) ) ) <_ _pi ) )
162 161 simprd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A + _i ) ) ) <_ _pi )
163 leneg 
 |-  ( ( ( Im ` ( log ` ( A + _i ) ) ) e. RR /\ _pi e. RR ) -> ( ( Im ` ( log ` ( A + _i ) ) ) <_ _pi <-> -u _pi <_ -u ( Im ` ( log ` ( A + _i ) ) ) ) )
164 142 123 163 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( A + _i ) ) ) <_ _pi <-> -u _pi <_ -u ( Im ` ( log ` ( A + _i ) ) ) ) )
165 162 164 mpbid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi <_ -u ( Im ` ( log ` ( A + _i ) ) ) )
166 157 157 139 158 160 165 ltleaddd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( -u _pi + -u _pi ) < ( ( Im ` ( log ` ( A - _i ) ) ) + -u ( Im ` ( log ` ( A + _i ) ) ) ) )
167 140 143 negsubd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( A - _i ) ) ) + -u ( Im ` ( log ` ( A + _i ) ) ) ) = ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) )
168 166 167 breqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( -u _pi + -u _pi ) < ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) )
169 156 168 eqbrtrrid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( -u _pi - _pi ) < ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) )
170 123 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> _pi e. RR )
171 157 170 151 ltsubaddd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( -u _pi - _pi ) < ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) <-> -u _pi < ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) ) )
172 169 171 mpbid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi < ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) )
173 0red 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 e. RR )
174 6 imcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` A ) e. RR )
175 peano2rem 
 |-  ( ( Im ` A ) e. RR -> ( ( Im ` A ) - 1 ) e. RR )
176 174 175 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` A ) - 1 ) e. RR )
177 peano2re 
 |-  ( ( Im ` A ) e. RR -> ( ( Im ` A ) + 1 ) e. RR )
178 174 177 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` A ) + 1 ) e. RR )
179 174 ltm1d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` A ) - 1 ) < ( Im ` A ) )
180 174 ltp1d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` A ) < ( ( Im ` A ) + 1 ) )
181 176 174 178 179 180 lttrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` A ) - 1 ) < ( ( Im ` A ) + 1 ) )
182 ltdiv1 
 |-  ( ( ( ( Im ` A ) - 1 ) e. RR /\ ( ( Im ` A ) + 1 ) e. RR /\ ( ( Re ` A ) e. RR /\ 0 < ( Re ` A ) ) ) -> ( ( ( Im ` A ) - 1 ) < ( ( Im ` A ) + 1 ) <-> ( ( ( Im ` A ) - 1 ) / ( Re ` A ) ) < ( ( ( Im ` A ) + 1 ) / ( Re ` A ) ) ) )
183 176 178 35 48 182 syl112anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` A ) - 1 ) < ( ( Im ` A ) + 1 ) <-> ( ( ( Im ` A ) - 1 ) / ( Re ` A ) ) < ( ( ( Im ` A ) + 1 ) / ( Re ` A ) ) ) )
184 181 183 mpbid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` A ) - 1 ) / ( Re ` A ) ) < ( ( ( Im ` A ) + 1 ) / ( Re ` A ) ) )
185 imsub 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( Im ` ( A - _i ) ) = ( ( Im ` A ) - ( Im ` _i ) ) )
186 6 2 185 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( A - _i ) ) = ( ( Im ` A ) - ( Im ` _i ) ) )
187 imi 
 |-  ( Im ` _i ) = 1
188 187 oveq2i 
 |-  ( ( Im ` A ) - ( Im ` _i ) ) = ( ( Im ` A ) - 1 )
189 186 188 eqtrdi 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( A - _i ) ) = ( ( Im ` A ) - 1 ) )
190 189 39 oveq12d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( A - _i ) ) / ( Re ` ( A - _i ) ) ) = ( ( ( Im ` A ) - 1 ) / ( Re ` A ) ) )
191 imadd 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( Im ` ( A + _i ) ) = ( ( Im ` A ) + ( Im ` _i ) ) )
192 6 2 191 sylancl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( A + _i ) ) = ( ( Im ` A ) + ( Im ` _i ) ) )
193 187 oveq2i 
 |-  ( ( Im ` A ) + ( Im ` _i ) ) = ( ( Im ` A ) + 1 )
194 192 193 eqtrdi 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( A + _i ) ) = ( ( Im ` A ) + 1 ) )
195 194 83 oveq12d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( A + _i ) ) / ( Re ` ( A + _i ) ) ) = ( ( ( Im ` A ) + 1 ) / ( Re ` A ) ) )
196 184 190 195 3brtr4d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( A - _i ) ) / ( Re ` ( A - _i ) ) ) < ( ( Im ` ( A + _i ) ) / ( Re ` ( A + _i ) ) ) )
197 tanarg 
 |-  ( ( ( A - _i ) e. CC /\ ( Re ` ( A - _i ) ) =/= 0 ) -> ( tan ` ( Im ` ( log ` ( A - _i ) ) ) ) = ( ( Im ` ( A - _i ) ) / ( Re ` ( A - _i ) ) ) )
198 30 42 197 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( tan ` ( Im ` ( log ` ( A - _i ) ) ) ) = ( ( Im ` ( A - _i ) ) / ( Re ` ( A - _i ) ) ) )
199 tanarg 
 |-  ( ( ( A + _i ) e. CC /\ ( Re ` ( A + _i ) ) =/= 0 ) -> ( tan ` ( Im ` ( log ` ( A + _i ) ) ) ) = ( ( Im ` ( A + _i ) ) / ( Re ` ( A + _i ) ) ) )
200 73 99 199 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( tan ` ( Im ` ( log ` ( A + _i ) ) ) ) = ( ( Im ` ( A + _i ) ) / ( Re ` ( A + _i ) ) ) )
201 196 198 200 3brtr4d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( tan ` ( Im ` ( log ` ( A - _i ) ) ) ) < ( tan ` ( Im ` ( log ` ( A + _i ) ) ) ) )
202 48 39 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` ( A - _i ) ) )
203 argregt0 
 |-  ( ( ( A - _i ) e. CC /\ 0 < ( Re ` ( A - _i ) ) ) -> ( Im ` ( log ` ( A - _i ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
204 30 202 203 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A - _i ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
205 48 83 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` ( A + _i ) ) )
206 argregt0 
 |-  ( ( ( A + _i ) e. CC /\ 0 < ( Re ` ( A + _i ) ) ) -> ( Im ` ( log ` ( A + _i ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
207 73 205 206 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A + _i ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
208 tanord 
 |-  ( ( ( Im ` ( log ` ( A - _i ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ ( Im ` ( log ` ( A + _i ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( Im ` ( log ` ( A - _i ) ) ) < ( Im ` ( log ` ( A + _i ) ) ) <-> ( tan ` ( Im ` ( log ` ( A - _i ) ) ) ) < ( tan ` ( Im ` ( log ` ( A + _i ) ) ) ) ) )
209 204 207 208 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( A - _i ) ) ) < ( Im ` ( log ` ( A + _i ) ) ) <-> ( tan ` ( Im ` ( log ` ( A - _i ) ) ) ) < ( tan ` ( Im ` ( log ` ( A + _i ) ) ) ) ) )
210 201 209 mpbird 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A - _i ) ) ) < ( Im ` ( log ` ( A + _i ) ) ) )
211 143 addid2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 0 + ( Im ` ( log ` ( A + _i ) ) ) ) = ( Im ` ( log ` ( A + _i ) ) ) )
212 210 211 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( A - _i ) ) ) < ( 0 + ( Im ` ( log ` ( A + _i ) ) ) ) )
213 139 142 173 ltsubaddd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) < 0 <-> ( Im ` ( log ` ( A - _i ) ) ) < ( 0 + ( Im ` ( log ` ( A + _i ) ) ) ) ) )
214 212 213 mpbird 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) < 0 )
215 151 173 170 214 ltadd1dd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) < ( 0 + _pi ) )
216 106 addid2i 
 |-  ( 0 + _pi ) = _pi
217 215 216 breqtrdi 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) < _pi )
218 154 rexri 
 |-  -u _pi e. RR*
219 123 rexri 
 |-  _pi e. RR*
220 elioo2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* ) -> ( ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) e. ( -u _pi (,) _pi ) <-> ( ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) e. RR /\ -u _pi < ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) /\ ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) < _pi ) ) )
221 218 219 220 mp2an 
 |-  ( ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) e. ( -u _pi (,) _pi ) <-> ( ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) e. RR /\ -u _pi < ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) /\ ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) < _pi ) )
222 153 172 217 221 syl3anbrc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( ( Im ` ( log ` ( A - _i ) ) ) - ( Im ` ( log ` ( A + _i ) ) ) ) + _pi ) e. ( -u _pi (,) _pi ) )
223 150 222 eqeltrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )