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