argimlt0

Description: Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015)

		Ref	Expression
	Assertion	argimlt0	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log A) \in (- π, 0)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (A) < 0$
2	1	lt0ne0d	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (A) \neq 0$
3		fveq2	$⊢ A = 0 \to ℑ (A) = ℑ (0)$
4		im0	$⊢ ℑ (0) = 0$
5	3 4	eqtrdi	$⊢ A = 0 \to ℑ (A) = 0$
6	5	necon3i	$⊢ ℑ (A) \neq 0 \to A \neq 0$
7	2 6	syl	$⊢ (A \in ℂ \land ℑ (A) < 0) \to A \neq 0$
8		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
9	7 8	syldan	$⊢ (A \in ℂ \land ℑ (A) < 0) \to \log A \in ℂ$
10	9	imcld	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log A) \in ℝ$
11		logcj	$⊢ (A \in ℂ \land ℑ (A) \neq 0) \to \log \overline{A} = \overline{\log A}$
12	2 11	syldan	$⊢ (A \in ℂ \land ℑ (A) < 0) \to \log \overline{A} = \overline{\log A}$
13	12	fveq2d	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log \overline{A}) = ℑ (\overline{\log A})$
14	9	imcjd	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\overline{\log A}) = - ℑ (\log A)$
15	13 14	eqtrd	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log \overline{A}) = - ℑ (\log A)$
16		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
17		imcl	$⊢ A \in ℂ \to ℑ (A) \in ℝ$
18	17	adantr	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (A) \in ℝ$
19	18	lt0neg1d	$⊢ (A \in ℂ \land ℑ (A) < 0) \to (ℑ (A) < 0 \leftrightarrow 0 < - ℑ (A))$
20	1 19	mpbid	$⊢ (A \in ℂ \land ℑ (A) < 0) \to 0 < - ℑ (A)$
21		imcj	$⊢ A \in ℂ \to ℑ (\overline{A}) = - ℑ (A)$
22	21	adantr	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\overline{A}) = - ℑ (A)$
23	20 22	breqtrrd	$⊢ (A \in ℂ \land ℑ (A) < 0) \to 0 < ℑ (\overline{A})$
24		argimgt0	$⊢ (\overline{A} \in ℂ \land 0 < ℑ (\overline{A})) \to ℑ (\log \overline{A}) \in (0, π)$
25	16 23 24	syl2an2r	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log \overline{A}) \in (0, π)$
26		eliooord	$⊢ ℑ (\log \overline{A}) \in (0, π) \to (0 < ℑ (\log \overline{A}) \land ℑ (\log \overline{A}) < π)$
27	25 26	syl	$⊢ (A \in ℂ \land ℑ (A) < 0) \to (0 < ℑ (\log \overline{A}) \land ℑ (\log \overline{A}) < π)$
28	27	simprd	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log \overline{A}) < π$
29	15 28	eqbrtrrd	$⊢ (A \in ℂ \land ℑ (A) < 0) \to - ℑ (\log A) < π$
30		pire	$⊢ π \in ℝ$
31		ltnegcon1	$⊢ (ℑ (\log A) \in ℝ \land π \in ℝ) \to (- ℑ (\log A) < π \leftrightarrow - π < ℑ (\log A))$
32	10 30 31	sylancl	$⊢ (A \in ℂ \land ℑ (A) < 0) \to (- ℑ (\log A) < π \leftrightarrow - π < ℑ (\log A))$
33	29 32	mpbid	$⊢ (A \in ℂ \land ℑ (A) < 0) \to - π < ℑ (\log A)$
34	27	simpld	$⊢ (A \in ℂ \land ℑ (A) < 0) \to 0 < ℑ (\log \overline{A})$
35	34 15	breqtrd	$⊢ (A \in ℂ \land ℑ (A) < 0) \to 0 < - ℑ (\log A)$
36	10	lt0neg1d	$⊢ (A \in ℂ \land ℑ (A) < 0) \to (ℑ (\log A) < 0 \leftrightarrow 0 < - ℑ (\log A))$
37	35 36	mpbird	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log A) < 0$
38	30	renegcli	$⊢ - π \in ℝ$
39	38	rexri	$⊢ - π \in ℝ^{*}$
40		0xr	$⊢ 0 \in ℝ^{*}$
41		elioo2	$⊢ (- π \in ℝ^{} \land 0 \in ℝ^{}) \to (ℑ (\log A) \in (- π, 0) \leftrightarrow (ℑ (\log A) \in ℝ \land - π < ℑ (\log A) \land ℑ (\log A) < 0))$
42	39 40 41	mp2an	$⊢ ℑ (\log A) \in (- π, 0) \leftrightarrow (ℑ (\log A) \in ℝ \land - π < ℑ (\log A) \land ℑ (\log A) < 0)$
43	10 33 37 42	syl3anbrc	$⊢ (A \in ℂ \land ℑ (A) < 0) \to ℑ (\log A) \in (- π, 0)$

Metamath Proof Explorer

Theorem argimlt0

Proof