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