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 ) )