Metamath Proof Explorer

Theorem logcnlem4

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 logcnlem4 
|- ( ph -> ( abs ` ( ( Im ` ( log ` A ) ) - ( Im ` ( log ` B ) ) ) ) < R )

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 1 ellogdm 
 |-  ( A e. D <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) )
9 8 simplbi 
 |-  ( A e. D -> A e. CC )
10 4 9 syl 
 |-  ( ph -> A e. CC )
11 1 logdmn0 
 |-  ( A e. D -> A =/= 0 )
12 4 11 syl 
 |-  ( ph -> A =/= 0 )
13 10 12 logcld 
 |-  ( ph -> ( log ` A ) e. CC )
14 13 imcld 
 |-  ( ph -> ( Im ` ( log ` A ) ) e. RR )
15 14 recnd 
 |-  ( ph -> ( Im ` ( log ` A ) ) e. CC )
16 1 ellogdm 
 |-  ( B e. D <-> ( B e. CC /\ ( B e. RR -> B e. RR+ ) ) )
17 16 simplbi 
 |-  ( B e. D -> B e. CC )
18 6 17 syl 
 |-  ( ph -> B e. CC )
19 1 logdmn0 
 |-  ( B e. D -> B =/= 0 )
20 6 19 syl 
 |-  ( ph -> B =/= 0 )
21 18 20 logcld 
 |-  ( ph -> ( log ` B ) e. CC )
22 21 imcld 
 |-  ( ph -> ( Im ` ( log ` B ) ) e. RR )
23 22 recnd 
 |-  ( ph -> ( Im ` ( log ` B ) ) e. CC )
24 15 23 abssubd 
 |-  ( ph -> ( abs ` ( ( Im ` ( log ` A ) ) - ( Im ` ( log ` B ) ) ) ) = ( abs ` ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) ) )
25 21 13 imsubd 
 |-  ( ph -> ( Im ` ( ( log ` B ) - ( log ` A ) ) ) = ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
26 efsub 
 |-  ( ( ( log ` B ) e. CC /\ ( log ` A ) e. CC ) -> ( exp ` ( ( log ` B ) - ( log ` A ) ) ) = ( ( exp ` ( log ` B ) ) / ( exp ` ( log ` A ) ) ) )
27 21 13 26 syl2anc 
 |-  ( ph -> ( exp ` ( ( log ` B ) - ( log ` A ) ) ) = ( ( exp ` ( log ` B ) ) / ( exp ` ( log ` A ) ) ) )
28 eflog 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( exp ` ( log ` B ) ) = B )
29 18 20 28 syl2anc 
 |-  ( ph -> ( exp ` ( log ` B ) ) = B )
30 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
31 10 12 30 syl2anc 
 |-  ( ph -> ( exp ` ( log ` A ) ) = A )
32 29 31 oveq12d 
 |-  ( ph -> ( ( exp ` ( log ` B ) ) / ( exp ` ( log ` A ) ) ) = ( B / A ) )
33 27 32 eqtrd 
 |-  ( ph -> ( exp ` ( ( log ` B ) - ( log ` A ) ) ) = ( B / A ) )
34 18 10 12 divcld 
 |-  ( ph -> ( B / A ) e. CC )
35 18 10 20 12 divne0d 
 |-  ( ph -> ( B / A ) =/= 0 )
36 21 13 subcld 
 |-  ( ph -> ( ( log ` B ) - ( log ` A ) ) e. CC )
37 1 2 3 4 5 6 7 logcnlem3 
 |-  ( ph -> ( -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) /\ ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi ) )
38 37 simpld 
 |-  ( ph -> -u _pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) )
39 38 25 breqtrrd 
 |-  ( ph -> -u _pi < ( Im ` ( ( log ` B ) - ( log ` A ) ) ) )
40 37 simprd 
 |-  ( ph -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ _pi )
41 25 40 eqbrtrd 
 |-  ( ph -> ( Im ` ( ( log ` B ) - ( log ` A ) ) ) <_ _pi )
42 ellogrn 
 |-  ( ( ( log ` B ) - ( log ` A ) ) e. ran log <-> ( ( ( log ` B ) - ( log ` A ) ) e. CC /\ -u _pi < ( Im ` ( ( log ` B ) - ( log ` A ) ) ) /\ ( Im ` ( ( log ` B ) - ( log ` A ) ) ) <_ _pi ) )
43 36 39 41 42 syl3anbrc 
 |-  ( ph -> ( ( log ` B ) - ( log ` A ) ) e. ran log )
44 logeftb 
 |-  ( ( ( B / A ) e. CC /\ ( B / A ) =/= 0 /\ ( ( log ` B ) - ( log ` A ) ) e. ran log ) -> ( ( log ` ( B / A ) ) = ( ( log ` B ) - ( log ` A ) ) <-> ( exp ` ( ( log ` B ) - ( log ` A ) ) ) = ( B / A ) ) )
45 34 35 43 44 syl3anc 
 |-  ( ph -> ( ( log ` ( B / A ) ) = ( ( log ` B ) - ( log ` A ) ) <-> ( exp ` ( ( log ` B ) - ( log ` A ) ) ) = ( B / A ) ) )
46 33 45 mpbird 
 |-  ( ph -> ( log ` ( B / A ) ) = ( ( log ` B ) - ( log ` A ) ) )
47 46 eqcomd 
 |-  ( ph -> ( ( log ` B ) - ( log ` A ) ) = ( log ` ( B / A ) ) )
48 47 fveq2d 
 |-  ( ph -> ( Im ` ( ( log ` B ) - ( log ` A ) ) ) = ( Im ` ( log ` ( B / A ) ) ) )
49 25 48 eqtr3d 
 |-  ( ph -> ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) = ( Im ` ( log ` ( B / A ) ) ) )
50 49 fveq2d 
 |-  ( ph -> ( abs ` ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) ) = ( abs ` ( Im ` ( log ` ( B / A ) ) ) ) )
51 24 50 eqtrd 
 |-  ( ph -> ( abs ` ( ( Im ` ( log ` A ) ) - ( Im ` ( log ` B ) ) ) ) = ( abs ` ( Im ` ( log ` ( B / A ) ) ) ) )
52 34 35 logcld 
 |-  ( ph -> ( log ` ( B / A ) ) e. CC )
53 52 imcld 
 |-  ( ph -> ( Im ` ( log ` ( B / A ) ) ) e. RR )
54 53 recnd 
 |-  ( ph -> ( Im ` ( log ` ( B / A ) ) ) e. CC )
55 54 abscld 
 |-  ( ph -> ( abs ` ( Im ` ( log ` ( B / A ) ) ) ) e. RR )
56 0red 
 |-  ( ph -> 0 e. RR )
57 1re 
 |-  1 e. RR
58 10 18 subcld 
 |-  ( ph -> ( A - B ) e. CC )
59 58 abscld 
 |-  ( ph -> ( abs ` ( A - B ) ) e. RR )
60 10 12 absrpcld 
 |-  ( ph -> ( abs ` A ) e. RR+ )
61 59 60 rerpdivcld 
 |-  ( ph -> ( ( abs ` ( A - B ) ) / ( abs ` A ) ) e. RR )
62 resubcl 
 |-  ( ( 1 e. RR /\ ( ( abs ` ( A - B ) ) / ( abs ` A ) ) e. RR ) -> ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) e. RR )
63 57 61 62 sylancr 
 |-  ( ph -> ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) e. RR )
64 34 recld 
 |-  ( ph -> ( Re ` ( B / A ) ) e. RR )
65 10 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
66 5 rpred 
 |-  ( ph -> R e. RR )
67 1rp 
 |-  1 e. RR+
68 rpaddcl 
 |-  ( ( 1 e. RR+ /\ R e. RR+ ) -> ( 1 + R ) e. RR+ )
69 67 5 68 sylancr 
 |-  ( ph -> ( 1 + R ) e. RR+ )
70 66 69 rerpdivcld 
 |-  ( ph -> ( R / ( 1 + R ) ) e. RR )
71 65 70 remulcld 
 |-  ( ph -> ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) e. RR )
72 3 71 eqeltrid 
 |-  ( ph -> T e. RR )
73 rpre 
 |-  ( A e. RR+ -> A e. RR )
74 73 adantl 
 |-  ( ( ph /\ A e. RR+ ) -> A e. RR )
75 10 imcld 
 |-  ( ph -> ( Im ` A ) e. RR )
76 75 recnd 
 |-  ( ph -> ( Im ` A ) e. CC )
77 76 abscld 
 |-  ( ph -> ( abs ` ( Im ` A ) ) e. RR )
78 77 adantr 
 |-  ( ( ph /\ -. A e. RR+ ) -> ( abs ` ( Im ` A ) ) e. RR )
79 74 78 ifclda 
 |-  ( ph -> if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) ) e. RR )
80 2 79 eqeltrid 
 |-  ( ph -> S e. RR )
81 ltmin 
 |-  ( ( ( abs ` ( A - B ) ) e. RR /\ S e. RR /\ T e. RR ) -> ( ( abs ` ( A - B ) ) < if ( S <_ T , S , T ) <-> ( ( abs ` ( A - B ) ) < S /\ ( abs ` ( A - B ) ) < T ) ) )
82 59 80 72 81 syl3anc 
 |-  ( ph -> ( ( abs ` ( A - B ) ) < if ( S <_ T , S , T ) <-> ( ( abs ` ( A - B ) ) < S /\ ( abs ` ( A - B ) ) < T ) ) )
83 7 82 mpbid 
 |-  ( ph -> ( ( abs ` ( A - B ) ) < S /\ ( abs ` ( A - B ) ) < T ) )
84 83 simprd 
 |-  ( ph -> ( abs ` ( A - B ) ) < T )
85 69 rpred 
 |-  ( ph -> ( 1 + R ) e. RR )
86 66 ltp1d 
 |-  ( ph -> R < ( R + 1 ) )
87 66 recnd 
 |-  ( ph -> R e. CC )
88 ax-1cn 
 |-  1 e. CC
89 addcom 
 |-  ( ( R e. CC /\ 1 e. CC ) -> ( R + 1 ) = ( 1 + R ) )
90 87 88 89 sylancl 
 |-  ( ph -> ( R + 1 ) = ( 1 + R ) )
91 86 90 breqtrd 
 |-  ( ph -> R < ( 1 + R ) )
92 66 85 91 ltled 
 |-  ( ph -> R <_ ( 1 + R ) )
93 85 recnd 
 |-  ( ph -> ( 1 + R ) e. CC )
94 93 mulid1d 
 |-  ( ph -> ( ( 1 + R ) x. 1 ) = ( 1 + R ) )
95 92 94 breqtrrd 
 |-  ( ph -> R <_ ( ( 1 + R ) x. 1 ) )
96 57 a1i 
 |-  ( ph -> 1 e. RR )
97 66 96 69 ledivmuld 
 |-  ( ph -> ( ( R / ( 1 + R ) ) <_ 1 <-> R <_ ( ( 1 + R ) x. 1 ) ) )
98 95 97 mpbird 
 |-  ( ph -> ( R / ( 1 + R ) ) <_ 1 )
99 70 96 60 lemul2d 
 |-  ( ph -> ( ( R / ( 1 + R ) ) <_ 1 <-> ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) <_ ( ( abs ` A ) x. 1 ) ) )
100 98 99 mpbid 
 |-  ( ph -> ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) <_ ( ( abs ` A ) x. 1 ) )
101 65 recnd 
 |-  ( ph -> ( abs ` A ) e. CC )
102 101 mulid1d 
 |-  ( ph -> ( ( abs ` A ) x. 1 ) = ( abs ` A ) )
103 100 102 breqtrd 
 |-  ( ph -> ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) <_ ( abs ` A ) )
104 3 103 eqbrtrid 
 |-  ( ph -> T <_ ( abs ` A ) )
105 59 72 65 84 104 ltletrd 
 |-  ( ph -> ( abs ` ( A - B ) ) < ( abs ` A ) )
106 105 102 breqtrrd 
 |-  ( ph -> ( abs ` ( A - B ) ) < ( ( abs ` A ) x. 1 ) )
107 59 96 60 ltdivmuld 
 |-  ( ph -> ( ( ( abs ` ( A - B ) ) / ( abs ` A ) ) < 1 <-> ( abs ` ( A - B ) ) < ( ( abs ` A ) x. 1 ) ) )
108 106 107 mpbird 
 |-  ( ph -> ( ( abs ` ( A - B ) ) / ( abs ` A ) ) < 1 )
109 posdif 
 |-  ( ( ( ( abs ` ( A - B ) ) / ( abs ` A ) ) e. RR /\ 1 e. RR ) -> ( ( ( abs ` ( A - B ) ) / ( abs ` A ) ) < 1 <-> 0 < ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) ) )
110 61 57 109 sylancl 
 |-  ( ph -> ( ( ( abs ` ( A - B ) ) / ( abs ` A ) ) < 1 <-> 0 < ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) ) )
111 108 110 mpbid 
 |-  ( ph -> 0 < ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) )
112 58 10 12 divcld 
 |-  ( ph -> ( ( A - B ) / A ) e. CC )
113 112 releabsd 
 |-  ( ph -> ( Re ` ( ( A - B ) / A ) ) <_ ( abs ` ( ( A - B ) / A ) ) )
114 10 18 10 12 divsubdird 
 |-  ( ph -> ( ( A - B ) / A ) = ( ( A / A ) - ( B / A ) ) )
115 10 12 dividd 
 |-  ( ph -> ( A / A ) = 1 )
116 115 oveq1d 
 |-  ( ph -> ( ( A / A ) - ( B / A ) ) = ( 1 - ( B / A ) ) )
117 114 116 eqtrd 
 |-  ( ph -> ( ( A - B ) / A ) = ( 1 - ( B / A ) ) )
118 117 fveq2d 
 |-  ( ph -> ( Re ` ( ( A - B ) / A ) ) = ( Re ` ( 1 - ( B / A ) ) ) )
119 resub 
 |-  ( ( 1 e. CC /\ ( B / A ) e. CC ) -> ( Re ` ( 1 - ( B / A ) ) ) = ( ( Re ` 1 ) - ( Re ` ( B / A ) ) ) )
120 88 34 119 sylancr 
 |-  ( ph -> ( Re ` ( 1 - ( B / A ) ) ) = ( ( Re ` 1 ) - ( Re ` ( B / A ) ) ) )
121 118 120 eqtrd 
 |-  ( ph -> ( Re ` ( ( A - B ) / A ) ) = ( ( Re ` 1 ) - ( Re ` ( B / A ) ) ) )
122 re1 
 |-  ( Re ` 1 ) = 1
123 122 oveq1i 
 |-  ( ( Re ` 1 ) - ( Re ` ( B / A ) ) ) = ( 1 - ( Re ` ( B / A ) ) )
124 121 123 eqtrdi 
 |-  ( ph -> ( Re ` ( ( A - B ) / A ) ) = ( 1 - ( Re ` ( B / A ) ) ) )
125 58 10 12 absdivd 
 |-  ( ph -> ( abs ` ( ( A - B ) / A ) ) = ( ( abs ` ( A - B ) ) / ( abs ` A ) ) )
126 113 124 125 3brtr3d 
 |-  ( ph -> ( 1 - ( Re ` ( B / A ) ) ) <_ ( ( abs ` ( A - B ) ) / ( abs ` A ) ) )
127 96 64 61 126 subled 
 |-  ( ph -> ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) <_ ( Re ` ( B / A ) ) )
128 56 63 64 111 127 ltletrd 
 |-  ( ph -> 0 < ( Re ` ( B / A ) ) )
129 argregt0 
 |-  ( ( ( B / A ) e. CC /\ 0 < ( Re ` ( B / A ) ) ) -> ( Im ` ( log ` ( B / A ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
130 34 128 129 syl2anc 
 |-  ( ph -> ( Im ` ( log ` ( B / A ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
131 cosq14gt0 
 |-  ( ( Im ` ( log ` ( B / A ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( cos ` ( Im ` ( log ` ( B / A ) ) ) ) )
132 130 131 syl 
 |-  ( ph -> 0 < ( cos ` ( Im ` ( log ` ( B / A ) ) ) ) )
133 132 gt0ne0d 
 |-  ( ph -> ( cos ` ( Im ` ( log ` ( B / A ) ) ) ) =/= 0 )
134 53 133 retancld 
 |-  ( ph -> ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) e. RR )
135 134 recnd 
 |-  ( ph -> ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) e. CC )
136 135 abscld 
 |-  ( ph -> ( abs ` ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) ) e. RR )
137 tanabsge 
 |-  ( ( Im ` ( log ` ( B / A ) ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( abs ` ( Im ` ( log ` ( B / A ) ) ) ) <_ ( abs ` ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) ) )
138 130 137 syl 
 |-  ( ph -> ( abs ` ( Im ` ( log ` ( B / A ) ) ) ) <_ ( abs ` ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) ) )
139 128 gt0ne0d 
 |-  ( ph -> ( Re ` ( B / A ) ) =/= 0 )
140 tanarg 
 |-  ( ( ( B / A ) e. CC /\ ( Re ` ( B / A ) ) =/= 0 ) -> ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) = ( ( Im ` ( B / A ) ) / ( Re ` ( B / A ) ) ) )
141 34 139 140 syl2anc 
 |-  ( ph -> ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) = ( ( Im ` ( B / A ) ) / ( Re ` ( B / A ) ) ) )
142 141 fveq2d 
 |-  ( ph -> ( abs ` ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) ) = ( abs ` ( ( Im ` ( B / A ) ) / ( Re ` ( B / A ) ) ) ) )
143 34 imcld 
 |-  ( ph -> ( Im ` ( B / A ) ) e. RR )
144 143 recnd 
 |-  ( ph -> ( Im ` ( B / A ) ) e. CC )
145 64 recnd 
 |-  ( ph -> ( Re ` ( B / A ) ) e. CC )
146 144 145 139 absdivd 
 |-  ( ph -> ( abs ` ( ( Im ` ( B / A ) ) / ( Re ` ( B / A ) ) ) ) = ( ( abs ` ( Im ` ( B / A ) ) ) / ( abs ` ( Re ` ( B / A ) ) ) ) )
147 56 64 128 ltled 
 |-  ( ph -> 0 <_ ( Re ` ( B / A ) ) )
148 64 147 absidd 
 |-  ( ph -> ( abs ` ( Re ` ( B / A ) ) ) = ( Re ` ( B / A ) ) )
149 148 oveq2d 
 |-  ( ph -> ( ( abs ` ( Im ` ( B / A ) ) ) / ( abs ` ( Re ` ( B / A ) ) ) ) = ( ( abs ` ( Im ` ( B / A ) ) ) / ( Re ` ( B / A ) ) ) )
150 142 146 149 3eqtrd 
 |-  ( ph -> ( abs ` ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) ) = ( ( abs ` ( Im ` ( B / A ) ) ) / ( Re ` ( B / A ) ) ) )
151 144 abscld 
 |-  ( ph -> ( abs ` ( Im ` ( B / A ) ) ) e. RR )
152 64 66 remulcld 
 |-  ( ph -> ( ( Re ` ( B / A ) ) x. R ) e. RR )
153 18 10 subcld 
 |-  ( ph -> ( B - A ) e. CC )
154 153 10 12 divcld 
 |-  ( ph -> ( ( B - A ) / A ) e. CC )
155 absimle 
 |-  ( ( ( B - A ) / A ) e. CC -> ( abs ` ( Im ` ( ( B - A ) / A ) ) ) <_ ( abs ` ( ( B - A ) / A ) ) )
156 154 155 syl 
 |-  ( ph -> ( abs ` ( Im ` ( ( B - A ) / A ) ) ) <_ ( abs ` ( ( B - A ) / A ) ) )
157 18 10 10 12 divsubdird 
 |-  ( ph -> ( ( B - A ) / A ) = ( ( B / A ) - ( A / A ) ) )
158 115 oveq2d 
 |-  ( ph -> ( ( B / A ) - ( A / A ) ) = ( ( B / A ) - 1 ) )
159 157 158 eqtrd 
 |-  ( ph -> ( ( B - A ) / A ) = ( ( B / A ) - 1 ) )
160 159 fveq2d 
 |-  ( ph -> ( Im ` ( ( B - A ) / A ) ) = ( Im ` ( ( B / A ) - 1 ) ) )
161 imsub 
 |-  ( ( ( B / A ) e. CC /\ 1 e. CC ) -> ( Im ` ( ( B / A ) - 1 ) ) = ( ( Im ` ( B / A ) ) - ( Im ` 1 ) ) )
162 34 88 161 sylancl 
 |-  ( ph -> ( Im ` ( ( B / A ) - 1 ) ) = ( ( Im ` ( B / A ) ) - ( Im ` 1 ) ) )
163 im1 
 |-  ( Im ` 1 ) = 0
164 163 oveq2i 
 |-  ( ( Im ` ( B / A ) ) - ( Im ` 1 ) ) = ( ( Im ` ( B / A ) ) - 0 )
165 162 164 eqtrdi 
 |-  ( ph -> ( Im ` ( ( B / A ) - 1 ) ) = ( ( Im ` ( B / A ) ) - 0 ) )
166 144 subid1d 
 |-  ( ph -> ( ( Im ` ( B / A ) ) - 0 ) = ( Im ` ( B / A ) ) )
167 160 165 166 3eqtrrd 
 |-  ( ph -> ( Im ` ( B / A ) ) = ( Im ` ( ( B - A ) / A ) ) )
168 167 fveq2d 
 |-  ( ph -> ( abs ` ( Im ` ( B / A ) ) ) = ( abs ` ( Im ` ( ( B - A ) / A ) ) ) )
169 10 18 abssubd 
 |-  ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
170 169 oveq1d 
 |-  ( ph -> ( ( abs ` ( A - B ) ) / ( abs ` A ) ) = ( ( abs ` ( B - A ) ) / ( abs ` A ) ) )
171 153 10 12 absdivd 
 |-  ( ph -> ( abs ` ( ( B - A ) / A ) ) = ( ( abs ` ( B - A ) ) / ( abs ` A ) ) )
172 170 171 eqtr4d 
 |-  ( ph -> ( ( abs ` ( A - B ) ) / ( abs ` A ) ) = ( abs ` ( ( B - A ) / A ) ) )
173 156 168 172 3brtr4d 
 |-  ( ph -> ( abs ` ( Im ` ( B / A ) ) ) <_ ( ( abs ` ( A - B ) ) / ( abs ` A ) ) )
174 65 59 resubcld 
 |-  ( ph -> ( ( abs ` A ) - ( abs ` ( A - B ) ) ) e. RR )
175 174 66 remulcld 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) x. R ) e. RR )
176 65 152 remulcld 
 |-  ( ph -> ( ( abs ` A ) x. ( ( Re ` ( B / A ) ) x. R ) ) e. RR )
177 59 recnd 
 |-  ( ph -> ( abs ` ( A - B ) ) e. CC )
178 88 a1i 
 |-  ( ph -> 1 e. CC )
179 177 178 87 adddid 
 |-  ( ph -> ( ( abs ` ( A - B ) ) x. ( 1 + R ) ) = ( ( ( abs ` ( A - B ) ) x. 1 ) + ( ( abs ` ( A - B ) ) x. R ) ) )
180 177 mulid1d 
 |-  ( ph -> ( ( abs ` ( A - B ) ) x. 1 ) = ( abs ` ( A - B ) ) )
181 180 oveq1d 
 |-  ( ph -> ( ( ( abs ` ( A - B ) ) x. 1 ) + ( ( abs ` ( A - B ) ) x. R ) ) = ( ( abs ` ( A - B ) ) + ( ( abs ` ( A - B ) ) x. R ) ) )
182 179 181 eqtrd 
 |-  ( ph -> ( ( abs ` ( A - B ) ) x. ( 1 + R ) ) = ( ( abs ` ( A - B ) ) + ( ( abs ` ( A - B ) ) x. R ) ) )
183 69 rpne0d 
 |-  ( ph -> ( 1 + R ) =/= 0 )
184 101 87 93 183 divassd 
 |-  ( ph -> ( ( ( abs ` A ) x. R ) / ( 1 + R ) ) = ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) )
185 184 3 eqtr4di 
 |-  ( ph -> ( ( ( abs ` A ) x. R ) / ( 1 + R ) ) = T )
186 84 185 breqtrrd 
 |-  ( ph -> ( abs ` ( A - B ) ) < ( ( ( abs ` A ) x. R ) / ( 1 + R ) ) )
187 65 66 remulcld 
 |-  ( ph -> ( ( abs ` A ) x. R ) e. RR )
188 59 187 69 ltmuldivd 
 |-  ( ph -> ( ( ( abs ` ( A - B ) ) x. ( 1 + R ) ) < ( ( abs ` A ) x. R ) <-> ( abs ` ( A - B ) ) < ( ( ( abs ` A ) x. R ) / ( 1 + R ) ) ) )
189 186 188 mpbird 
 |-  ( ph -> ( ( abs ` ( A - B ) ) x. ( 1 + R ) ) < ( ( abs ` A ) x. R ) )
190 182 189 eqbrtrrd 
 |-  ( ph -> ( ( abs ` ( A - B ) ) + ( ( abs ` ( A - B ) ) x. R ) ) < ( ( abs ` A ) x. R ) )
191 59 66 remulcld 
 |-  ( ph -> ( ( abs ` ( A - B ) ) x. R ) e. RR )
192 59 191 187 ltaddsubd 
 |-  ( ph -> ( ( ( abs ` ( A - B ) ) + ( ( abs ` ( A - B ) ) x. R ) ) < ( ( abs ` A ) x. R ) <-> ( abs ` ( A - B ) ) < ( ( ( abs ` A ) x. R ) - ( ( abs ` ( A - B ) ) x. R ) ) ) )
193 190 192 mpbid 
 |-  ( ph -> ( abs ` ( A - B ) ) < ( ( ( abs ` A ) x. R ) - ( ( abs ` ( A - B ) ) x. R ) ) )
194 101 177 87 subdird 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) x. R ) = ( ( ( abs ` A ) x. R ) - ( ( abs ` ( A - B ) ) x. R ) ) )
195 193 194 breqtrrd 
 |-  ( ph -> ( abs ` ( A - B ) ) < ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) x. R ) )
196 60 rpne0d 
 |-  ( ph -> ( abs ` A ) =/= 0 )
197 101 177 101 196 divsubdird 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) / ( abs ` A ) ) = ( ( ( abs ` A ) / ( abs ` A ) ) - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) )
198 101 196 dividd 
 |-  ( ph -> ( ( abs ` A ) / ( abs ` A ) ) = 1 )
199 198 oveq1d 
 |-  ( ph -> ( ( ( abs ` A ) / ( abs ` A ) ) - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) = ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) )
200 197 199 eqtrd 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) / ( abs ` A ) ) = ( 1 - ( ( abs ` ( A - B ) ) / ( abs ` A ) ) ) )
201 200 127 eqbrtrd 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) / ( abs ` A ) ) <_ ( Re ` ( B / A ) ) )
202 174 64 60 ledivmuld 
 |-  ( ph -> ( ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) / ( abs ` A ) ) <_ ( Re ` ( B / A ) ) <-> ( ( abs ` A ) - ( abs ` ( A - B ) ) ) <_ ( ( abs ` A ) x. ( Re ` ( B / A ) ) ) ) )
203 201 202 mpbid 
 |-  ( ph -> ( ( abs ` A ) - ( abs ` ( A - B ) ) ) <_ ( ( abs ` A ) x. ( Re ` ( B / A ) ) ) )
204 65 64 remulcld 
 |-  ( ph -> ( ( abs ` A ) x. ( Re ` ( B / A ) ) ) e. RR )
205 174 204 5 lemul1d 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) <_ ( ( abs ` A ) x. ( Re ` ( B / A ) ) ) <-> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) x. R ) <_ ( ( ( abs ` A ) x. ( Re ` ( B / A ) ) ) x. R ) ) )
206 203 205 mpbid 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) x. R ) <_ ( ( ( abs ` A ) x. ( Re ` ( B / A ) ) ) x. R ) )
207 101 145 87 mulassd 
 |-  ( ph -> ( ( ( abs ` A ) x. ( Re ` ( B / A ) ) ) x. R ) = ( ( abs ` A ) x. ( ( Re ` ( B / A ) ) x. R ) ) )
208 206 207 breqtrd 
 |-  ( ph -> ( ( ( abs ` A ) - ( abs ` ( A - B ) ) ) x. R ) <_ ( ( abs ` A ) x. ( ( Re ` ( B / A ) ) x. R ) ) )
209 59 175 176 195 208 ltletrd 
 |-  ( ph -> ( abs ` ( A - B ) ) < ( ( abs ` A ) x. ( ( Re ` ( B / A ) ) x. R ) ) )
210 59 152 60 ltdivmuld 
 |-  ( ph -> ( ( ( abs ` ( A - B ) ) / ( abs ` A ) ) < ( ( Re ` ( B / A ) ) x. R ) <-> ( abs ` ( A - B ) ) < ( ( abs ` A ) x. ( ( Re ` ( B / A ) ) x. R ) ) ) )
211 209 210 mpbird 
 |-  ( ph -> ( ( abs ` ( A - B ) ) / ( abs ` A ) ) < ( ( Re ` ( B / A ) ) x. R ) )
212 151 61 152 173 211 lelttrd 
 |-  ( ph -> ( abs ` ( Im ` ( B / A ) ) ) < ( ( Re ` ( B / A ) ) x. R ) )
213 ltdivmul 
 |-  ( ( ( abs ` ( Im ` ( B / A ) ) ) e. RR /\ R e. RR /\ ( ( Re ` ( B / A ) ) e. RR /\ 0 < ( Re ` ( B / A ) ) ) ) -> ( ( ( abs ` ( Im ` ( B / A ) ) ) / ( Re ` ( B / A ) ) ) < R <-> ( abs ` ( Im ` ( B / A ) ) ) < ( ( Re ` ( B / A ) ) x. R ) ) )
214 151 66 64 128 213 syl112anc 
 |-  ( ph -> ( ( ( abs ` ( Im ` ( B / A ) ) ) / ( Re ` ( B / A ) ) ) < R <-> ( abs ` ( Im ` ( B / A ) ) ) < ( ( Re ` ( B / A ) ) x. R ) ) )
215 212 214 mpbird 
 |-  ( ph -> ( ( abs ` ( Im ` ( B / A ) ) ) / ( Re ` ( B / A ) ) ) < R )
216 150 215 eqbrtrd 
 |-  ( ph -> ( abs ` ( tan ` ( Im ` ( log ` ( B / A ) ) ) ) ) < R )
217 55 136 66 138 216 lelttrd 
 |-  ( ph -> ( abs ` ( Im ` ( log ` ( B / A ) ) ) ) < R )
218 51 217 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( Im ` ( log ` A ) ) - ( Im ` ( log ` B ) ) ) ) < R )