Metamath Proof Explorer

Theorem logcnlem4

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

Ref Expression
Hypotheses logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
logcnlem.s ⊢ 𝑆 = if ( 𝐴 ∈ ℝ+ , 𝐴 , ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
logcnlem.t ⊢ 𝑇 = ( ( abs ‘ 𝐴 ) · ( 𝑅 / ( 1 + 𝑅 ) ) )
logcnlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
logcnlem.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
logcnlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
logcnlem.l ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) < if ( 𝑆 ≤ 𝑇 , 𝑆 , 𝑇 ) )
Assertion logcnlem4 ( 𝜑 → ( abs ‘ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − ( ℑ ‘ ( log ‘ 𝐵 ) ) ) ) < 𝑅 )

Proof

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