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	mulridd	⊢ ( 𝜑 → ( ( 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	mulridd	⊢ ( 𝜑 → ( ( 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	mulridd	⊢ ( 𝜑 → ( ( 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 ‘ 𝐵 ) ) ) ) < 𝑅 )