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	imbitrid	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ+ → ( ℑ ‘ 𝐴 ) = 0 ) )
112	111	necon3ad	⊢ ( 𝜑 → ( ( ℑ ‘ 𝐴 ) ≠ 0 → ¬ 𝐴 ∈ ℝ+ ) )
113	112	imp	⊢ ( ( 𝜑 ∧ ( ℑ ‘ 𝐴 ) ≠ 0 ) → ¬ 𝐴 ∈ ℝ+ )
114		iffalse	⊢ ( ¬ 𝐴 ∈ ℝ+ → if ( 𝐴 ∈ ℝ+ , 𝐴 , ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) = ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
115	2 114	eqtrid	⊢ ( ¬ 𝐴 ∈ ℝ+ → 𝑆 = ( 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 ‘ 𝐴 ) ) ) ≤ π ) )