Metamath Proof Explorer

Theorem logcnlem3

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