Theorem logcnlem3

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

	Ref	Expression
Hypotheses	logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
	logcnlem.s	$$⊢S=if\left(A\in {ℝ}^{+},A,\left|\Im \left(A\right)\right|\right)$$
	logcnlem.t	$$⊢T=\left|A\right|\left(\frac{R}{1+R}\right)$$
	logcnlem.a	$$⊢\phi \to A\in D$$
	logcnlem.r	$$⊢\phi \to R\in {ℝ}^{+}$$
	logcnlem.b	$$⊢\phi \to B\in D$$
	logcnlem.l	$$⊢\phi \to \left|A-B\right|<if\left(S\le T,S,T\right)$$
Assertion	logcnlem3	$$⊢\phi \to \left(-\mathrm{\pi }<\Im \left(\log B\right)-\Im \left(\log A\right)\wedge \Im \left(\log B\right)-\Im \left(\log A\right)\le \mathrm{\pi }\right)$$

Proof

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