Theorem logcnlem4

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	logcnlem4	$$⊢\phi \to \left|\Im \left(\log A\right)-\Im \left(\log B\right)\right|<R$$

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