Metamath Proof Explorer

Theorem logcnlem3

Description: Lemma for logcn . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Hypotheses logcn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
logcnlem.s 
|- S = if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) )
logcnlem.t 
|- T = ( ( abs ` A ) x. ( R / ( 1 + R ) ) )
logcnlem.a 
|- ( ph -> A e. D )
logcnlem.r 
|- ( ph -> R e. RR+ )
logcnlem.b 
|- ( ph -> B e. D )
logcnlem.l 
|- ( ph -> ( abs ` ( A - B ) ) < if ( S <_ T , S , T ) )
Assertion logcnlem3 
|- ( ph -> ( -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) /\ ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi ) )

Proof

Step Hyp Ref Expression
1 logcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 logcnlem.s 
 |-  S = if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) )
3 logcnlem.t 
 |-  T = ( ( abs ` A ) x. ( R / ( 1 + R ) ) )
4 logcnlem.a 
 |-  ( ph -> A e. D )
5 logcnlem.r 
 |-  ( ph -> R e. RR+ )
6 logcnlem.b 
 |-  ( ph -> B e. D )
7 logcnlem.l 
 |-  ( ph -> ( abs ` ( A - B ) ) < if ( S <_ T , S , T ) )
8 pire 
 |-  _pi e. RR
9 8 renegcli 
 |-  -u _pi e. RR
10 9 a1i 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u _pi e. RR )
11 1 ellogdm 
 |-  ( B e. D <-> ( B e. CC /\ ( B e. RR -> B e. RR+ ) ) )
12 11 simplbi 
 |-  ( B e. D -> B e. CC )
13 6 12 syl 
 |-  ( ph -> B e. CC )
14 1 logdmn0 
 |-  ( B e. D -> B =/= 0 )
15 6 14 syl 
 |-  ( ph -> B =/= 0 )
16 13 15 logcld 
 |-  ( ph -> ( log ` B ) e. CC )
17 16 imcld 
 |-  ( ph -> ( Im ` ( log ` B ) ) e. RR )
18 17 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` B ) ) e. RR )
19 1 ellogdm 
 |-  ( A e. D <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) )
20 19 simplbi 
 |-  ( A e. D -> A e. CC )
21 4 20 syl 
 |-  ( ph -> A e. CC )
22 1 logdmn0 
 |-  ( A e. D -> A =/= 0 )
23 4 22 syl 
 |-  ( ph -> A =/= 0 )
24 21 23 logcld 
 |-  ( ph -> ( log ` A ) e. CC )
25 24 imcld 
 |-  ( ph -> ( Im ` ( log ` A ) ) e. RR )
26 17 25 resubcld 
 |-  ( ph -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) e. RR )
27 26 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) e. RR )
28 13 15 logimcld 
 |-  ( ph -> ( -u _pi < ( Im ` ( log ` B ) ) /\ ( Im ` ( log ` B ) ) <_ _pi ) )
29 28 simpld 
 |-  ( ph -> -u _pi < ( Im ` ( log ` B ) ) )
30 29 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u _pi < ( Im ` ( log ` B ) ) )
31 17 recnd 
 |-  ( ph -> ( Im ` ( log ` B ) ) e. CC )
32 31 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` B ) ) e. CC )
33 32 subid1d 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` B ) ) - 0 ) = ( Im ` ( log ` B ) ) )
34 25 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. RR )
35 0red 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> 0 e. RR )
36 argimlt0 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) )
37 21 36 sylan 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) )
38 eliooord 
 |-  ( ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < 0 ) )
39 37 38 syl 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < 0 ) )
40 39 simprd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) < 0 )
41 34 35 18 40 ltsub2dd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` B ) ) - 0 ) < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
42 33 41 eqbrtrrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` B ) ) < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
43 10 18 27 30 42 lttrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
44 29 adantr 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> -u _pi < ( Im ` ( log ` B ) ) )
45 reim0b 
 |-  ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
46 21 45 syl 
 |-  ( ph -> ( A e. RR <-> ( Im ` A ) = 0 ) )
47 19 simprbi 
 |-  ( A e. D -> ( A e. RR -> A e. RR+ ) )
48 4 47 syl 
 |-  ( ph -> ( A e. RR -> A e. RR+ ) )
49 46 48 sylbird 
 |-  ( ph -> ( ( Im ` A ) = 0 -> A e. RR+ ) )
50 49 imp 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> A e. RR+ )
51 50 relogcld 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( log ` A ) e. RR )
52 51 reim0d 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( Im ` ( log ` A ) ) = 0 )
53 52 oveq2d 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) = ( ( Im ` ( log ` B ) ) - 0 ) )
54 31 subid1d 
 |-  ( ph -> ( ( Im ` ( log ` B ) ) - 0 ) = ( Im ` ( log ` B ) ) )
55 54 adantr 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( ( Im ` ( log ` B ) ) - 0 ) = ( Im ` ( log ` B ) ) )
56 53 55 eqtrd 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) = ( Im ` ( log ` B ) ) )
57 44 56 breqtrrd 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
58 9 a1i 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> -u _pi e. RR )
59 25 renegcld 
 |-  ( ph -> -u ( Im ` ( log ` A ) ) e. RR )
60 59 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> -u ( Im ` ( log ` A ) ) e. RR )
61 26 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) e. RR )
62 argimgt0 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) )
63 21 62 sylan 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) )
64 eliooord 
 |-  ( ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) -> ( 0 < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < _pi ) )
65 63 64 syl 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < _pi ) )
66 65 simprd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) < _pi )
67 ltneg 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( ( Im ` ( log ` A ) ) < _pi <-> -u _pi < -u ( Im ` ( log ` A ) ) ) )
68 25 8 67 sylancl 
 |-  ( ph -> ( ( Im ` ( log ` A ) ) < _pi <-> -u _pi < -u ( Im ` ( log ` A ) ) ) )
69 68 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) < _pi <-> -u _pi < -u ( Im ` ( log ` A ) ) ) )
70 66 69 mpbid 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> -u _pi < -u ( Im ` ( log ` A ) ) )
71 df-neg 
 |-  -u ( Im ` ( log ` A ) ) = ( 0 - ( Im ` ( log ` A ) ) )
72 13 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> B e. CC )
73 21 13 imsubd 
 |-  ( ph -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
74 73 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
75 21 13 subcld 
 |-  ( ph -> ( A - B ) e. CC )
76 75 imcld 
 |-  ( ph -> ( Im ` ( A - B ) ) e. RR )
77 76 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( A - B ) ) e. RR )
78 75 abscld 
 |-  ( ph -> ( abs ` ( A - B ) ) e. RR )
79 78 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( abs ` ( A - B ) ) e. RR )
80 21 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> A e. CC )
81 80 imcld 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` A ) e. RR )
82 absimle 
 |-  ( ( A - B ) e. CC -> ( abs ` ( Im ` ( A - B ) ) ) <_ ( abs ` ( A - B ) ) )
83 75 82 syl 
 |-  ( ph -> ( abs ` ( Im ` ( A - B ) ) ) <_ ( abs ` ( A - B ) ) )
84 76 78 absled 
 |-  ( ph -> ( ( abs ` ( Im ` ( A - B ) ) ) <_ ( abs ` ( A - B ) ) <-> ( -u ( abs ` ( A - B ) ) <_ ( Im ` ( A - B ) ) /\ ( Im ` ( A - B ) ) <_ ( abs ` ( A - B ) ) ) ) )
85 83 84 mpbid 
 |-  ( ph -> ( -u ( abs ` ( A - B ) ) <_ ( Im ` ( A - B ) ) /\ ( Im ` ( A - B ) ) <_ ( abs ` ( A - B ) ) ) )
86 85 simprd 
 |-  ( ph -> ( Im ` ( A - B ) ) <_ ( abs ` ( A - B ) ) )
87 86 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( A - B ) ) <_ ( abs ` ( A - B ) ) )
88 rpre 
 |-  ( A e. RR+ -> A e. RR )
89 88 adantl 
 |-  ( ( ph /\ A e. RR+ ) -> A e. RR )
90 21 imcld 
 |-  ( ph -> ( Im ` A ) e. RR )
91 90 recnd 
 |-  ( ph -> ( Im ` A ) e. CC )
92 91 abscld 
 |-  ( ph -> ( abs ` ( Im ` A ) ) e. RR )
93 92 adantr 
 |-  ( ( ph /\ -. A e. RR+ ) -> ( abs ` ( Im ` A ) ) e. RR )
94 89 93 ifclda 
 |-  ( ph -> if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) ) e. RR )
95 2 94 eqeltrid 
 |-  ( ph -> S e. RR )
96 21 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
97 5 rpred 
 |-  ( ph -> R e. RR )
98 1rp 
 |-  1 e. RR+
99 rpaddcl 
 |-  ( ( 1 e. RR+ /\ R e. RR+ ) -> ( 1 + R ) e. RR+ )
100 98 5 99 sylancr 
 |-  ( ph -> ( 1 + R ) e. RR+ )
101 97 100 rerpdivcld 
 |-  ( ph -> ( R / ( 1 + R ) ) e. RR )
102 96 101 remulcld 
 |-  ( ph -> ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) e. RR )
103 3 102 eqeltrid 
 |-  ( ph -> T e. RR )
104 95 103 ifcld 
 |-  ( ph -> if ( S <_ T , S , T ) e. RR )
105 min1 
 |-  ( ( S e. RR /\ T e. RR ) -> if ( S <_ T , S , T ) <_ S )
106 95 103 105 syl2anc 
 |-  ( ph -> if ( S <_ T , S , T ) <_ S )
107 78 104 95 7 106 ltletrd 
 |-  ( ph -> ( abs ` ( A - B ) ) < S )
108 107 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( abs ` ( A - B ) ) < S )
109 gt0ne0 
 |-  ( ( ( Im ` A ) e. RR /\ 0 < ( Im ` A ) ) -> ( Im ` A ) =/= 0 )
110 90 109 sylan 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` A ) =/= 0 )
111 88 46 syl5ib 
 |-  ( ph -> ( A e. RR+ -> ( Im ` A ) = 0 ) )
112 111 necon3ad 
 |-  ( ph -> ( ( Im ` A ) =/= 0 -> -. A e. RR+ ) )
113 112 imp 
 |-  ( ( ph /\ ( Im ` A ) =/= 0 ) -> -. A e. RR+ )
114 iffalse 
 |-  ( -. A e. RR+ -> if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) ) = ( abs ` ( Im ` A ) ) )
115 2 114 syl5eq 
 |-  ( -. A e. RR+ -> S = ( abs ` ( Im ` A ) ) )
116 113 115 syl 
 |-  ( ( ph /\ ( Im ` A ) =/= 0 ) -> S = ( abs ` ( Im ` A ) ) )
117 110 116 syldan 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> S = ( abs ` ( Im ` A ) ) )
118 0re 
 |-  0 e. RR
119 ltle 
 |-  ( ( 0 e. RR /\ ( Im ` A ) e. RR ) -> ( 0 < ( Im ` A ) -> 0 <_ ( Im ` A ) ) )
120 118 90 119 sylancr 
 |-  ( ph -> ( 0 < ( Im ` A ) -> 0 <_ ( Im ` A ) ) )
121 120 imp 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> 0 <_ ( Im ` A ) )
122 81 121 absidd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( abs ` ( Im ` A ) ) = ( Im ` A ) )
123 117 122 eqtrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> S = ( Im ` A ) )
124 108 123 breqtrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( abs ` ( A - B ) ) < ( Im ` A ) )
125 77 79 81 87 124 lelttrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( A - B ) ) < ( Im ` A ) )
126 74 125 eqbrtrrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` A ) - ( Im ` B ) ) < ( Im ` A ) )
127 91 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` A ) e. CC )
128 127 subid1d 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` A ) - 0 ) = ( Im ` A ) )
129 126 128 breqtrrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` A ) - ( Im ` B ) ) < ( ( Im ` A ) - 0 ) )
130 0red 
 |-  ( ph -> 0 e. RR )
131 13 imcld 
 |-  ( ph -> ( Im ` B ) e. RR )
132 130 131 90 ltsub2d 
 |-  ( ph -> ( 0 < ( Im ` B ) <-> ( ( Im ` A ) - ( Im ` B ) ) < ( ( Im ` A ) - 0 ) ) )
133 132 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` B ) <-> ( ( Im ` A ) - ( Im ` B ) ) < ( ( Im ` A ) - 0 ) ) )
134 129 133 mpbird 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` B ) )
135 argimgt0 
 |-  ( ( B e. CC /\ 0 < ( Im ` B ) ) -> ( Im ` ( log ` B ) ) e. ( 0 (,) _pi ) )
136 72 134 135 syl2anc 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` B ) ) e. ( 0 (,) _pi ) )
137 eliooord 
 |-  ( ( Im ` ( log ` B ) ) e. ( 0 (,) _pi ) -> ( 0 < ( Im ` ( log ` B ) ) /\ ( Im ` ( log ` B ) ) < _pi ) )
138 136 137 syl 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` ( log ` B ) ) /\ ( Im ` ( log ` B ) ) < _pi ) )
139 138 simpld 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` ( log ` B ) ) )
140 130 17 25 ltsub1d 
 |-  ( ph -> ( 0 < ( Im ` ( log ` B ) ) <-> ( 0 - ( Im ` ( log ` A ) ) ) < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) ) )
141 140 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` ( log ` B ) ) <-> ( 0 - ( Im ` ( log ` A ) ) ) < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) ) )
142 139 141 mpbid 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( 0 - ( Im ` ( log ` A ) ) ) < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
143 71 142 eqbrtrid 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> -u ( Im ` ( log ` A ) ) < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
144 58 60 61 70 143 lttrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
145 lttri4 
 |-  ( ( ( Im ` A ) e. RR /\ 0 e. RR ) -> ( ( Im ` A ) < 0 \/ ( Im ` A ) = 0 \/ 0 < ( Im ` A ) ) )
146 90 118 145 sylancl 
 |-  ( ph -> ( ( Im ` A ) < 0 \/ ( Im ` A ) = 0 \/ 0 < ( Im ` A ) ) )
147 43 57 144 146 mpjao3dan 
 |-  ( ph -> -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
148 8 a1i 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> _pi e. RR )
149 34 renegcld 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u ( Im ` ( log ` A ) ) e. RR )
150 13 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> B e. CC )
151 91 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` A ) e. CC )
152 151 subid1d 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` A ) - 0 ) = ( Im ` A ) )
153 90 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` A ) e. RR )
154 78 renegcld 
 |-  ( ph -> -u ( abs ` ( A - B ) ) e. RR )
155 154 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u ( abs ` ( A - B ) ) e. RR )
156 76 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( A - B ) ) e. RR )
157 78 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( abs ` ( A - B ) ) e. RR )
158 107 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( abs ` ( A - B ) ) < S )
159 118 ltnri 
 |-  -. 0 < 0
160 breq1 
 |-  ( ( Im ` A ) = 0 -> ( ( Im ` A ) < 0 <-> 0 < 0 ) )
161 159 160 mtbiri 
 |-  ( ( Im ` A ) = 0 -> -. ( Im ` A ) < 0 )
162 161 necon2ai 
 |-  ( ( Im ` A ) < 0 -> ( Im ` A ) =/= 0 )
163 162 116 sylan2 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> S = ( abs ` ( Im ` A ) ) )
164 ltle 
 |-  ( ( ( Im ` A ) e. RR /\ 0 e. RR ) -> ( ( Im ` A ) < 0 -> ( Im ` A ) <_ 0 ) )
165 90 118 164 sylancl 
 |-  ( ph -> ( ( Im ` A ) < 0 -> ( Im ` A ) <_ 0 ) )
166 165 imp 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` A ) <_ 0 )
167 153 166 absnidd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( abs ` ( Im ` A ) ) = -u ( Im ` A ) )
168 163 167 eqtrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> S = -u ( Im ` A ) )
169 158 168 breqtrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( abs ` ( A - B ) ) < -u ( Im ` A ) )
170 157 153 169 ltnegcon2d 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` A ) < -u ( abs ` ( A - B ) ) )
171 85 simpld 
 |-  ( ph -> -u ( abs ` ( A - B ) ) <_ ( Im ` ( A - B ) ) )
172 171 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u ( abs ` ( A - B ) ) <_ ( Im ` ( A - B ) ) )
173 153 155 156 170 172 ltletrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` A ) < ( Im ` ( A - B ) ) )
174 73 adantr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
175 173 174 breqtrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` A ) < ( ( Im ` A ) - ( Im ` B ) ) )
176 152 175 eqbrtrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` A ) - 0 ) < ( ( Im ` A ) - ( Im ` B ) ) )
177 150 imcld 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` B ) e. RR )
178 177 35 153 ltsub2d 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` B ) < 0 <-> ( ( Im ` A ) - 0 ) < ( ( Im ` A ) - ( Im ` B ) ) ) )
179 176 178 mpbird 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` B ) < 0 )
180 argimlt0 
 |-  ( ( B e. CC /\ ( Im ` B ) < 0 ) -> ( Im ` ( log ` B ) ) e. ( -u _pi (,) 0 ) )
181 150 179 180 syl2anc 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` B ) ) e. ( -u _pi (,) 0 ) )
182 eliooord 
 |-  ( ( Im ` ( log ` B ) ) e. ( -u _pi (,) 0 ) -> ( -u _pi < ( Im ` ( log ` B ) ) /\ ( Im ` ( log ` B ) ) < 0 ) )
183 181 182 syl 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( -u _pi < ( Im ` ( log ` B ) ) /\ ( Im ` ( log ` B ) ) < 0 ) )
184 183 simprd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` B ) ) < 0 )
185 18 35 34 184 ltsub1dd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) < ( 0 - ( Im ` ( log ` A ) ) ) )
186 185 71 breqtrrdi 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) < -u ( Im ` ( log ` A ) ) )
187 39 simpld 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u _pi < ( Im ` ( log ` A ) ) )
188 ltnegcon1 
 |-  ( ( _pi e. RR /\ ( Im ` ( log ` A ) ) e. RR ) -> ( -u _pi < ( Im ` ( log ` A ) ) <-> -u ( Im ` ( log ` A ) ) < _pi ) )
189 8 34 188 sylancr 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) <-> -u ( Im ` ( log ` A ) ) < _pi ) )
190 187 189 mpbid 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> -u ( Im ` ( log ` A ) ) < _pi )
191 27 149 148 186 190 lttrd 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) < _pi )
192 27 148 191 ltled 
 |-  ( ( ph /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi )
193 28 simprd 
 |-  ( ph -> ( Im ` ( log ` B ) ) <_ _pi )
194 193 adantr 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( Im ` ( log ` B ) ) <_ _pi )
195 56 194 eqbrtrd 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi )
196 8 a1i 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> _pi e. RR )
197 17 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` B ) ) e. RR )
198 0red 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> 0 e. RR )
199 25 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. RR )
200 65 simpld 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` ( log ` A ) ) )
201 198 199 197 200 ltsub2dd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) < ( ( Im ` ( log ` B ) ) - 0 ) )
202 31 adantr 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` B ) ) e. CC )
203 202 subid1d 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` B ) ) - 0 ) = ( Im ` ( log ` B ) ) )
204 201 203 breqtrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) < ( Im ` ( log ` B ) ) )
205 138 simprd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` B ) ) < _pi )
206 61 197 196 204 205 lttrd 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) < _pi )
207 61 196 206 ltled 
 |-  ( ( ph /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi )
208 192 195 207 146 mpjao3dan 
 |-  ( ph -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi )
209 147 208 jca 
 |-  ( ph -> ( -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) /\ ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi ) )