logcnlem3

	Ref	Expression
Hypotheses	logcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
	logcnlem.s	$⊢ S = if (A \in ℝ^{+}, A, \|ℑ (A)\|)$
	logcnlem.t	$⊢ T = \|A\| (\frac{R}{1 + R})$
	logcnlem.a	$⊢ φ \to A \in D$
	logcnlem.r	$⊢ φ \to R \in ℝ^{+}$
	logcnlem.b	$⊢ φ \to B \in D$
	logcnlem.l	$⊢ φ \to \|A - B\| < if (S \leq T, S, T)$
Assertion	logcnlem3	$⊢ φ \to (- π < ℑ (\log B) - ℑ (\log A) \land ℑ (\log B) - ℑ (\log A) \leq π)$

Proof

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

Metamath Proof Explorer

Theorem logcnlem3

Proof