Theorem 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 e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` A ) < 0 )
2	1	lt0ne0d	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` A ) =/= 0 )
3		fveq2	|- ( A = 0 -> ( Im ` A ) = ( Im ` 0 ) )
4		im0	|- ( Im ` 0 ) = 0
5	3 4	eqtrdi	|- ( A = 0 -> ( Im ` A ) = 0 )
6	5	necon3i	|- ( ( Im ` A ) =/= 0 -> A =/= 0 )
7	2 6	syl	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> A =/= 0 )
8		logcl	|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
9	7 8	syldan	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( log ` A ) e. CC )
10	9	imcld	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. RR )
11		logcj	|- ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )
12	2 11	syldan	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )
13	12	fveq2d	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) = ( Im ` ( * ` ( log ` A ) ) ) )
14	9	imcjd	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( * ` ( log ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
15	13 14	eqtrd	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
16		cjcl	|- ( A e. CC -> ( * ` A ) e. CC )
17		imcl	|- ( A e. CC -> ( Im ` A ) e. RR )
18	17	adantr	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` A ) e. RR )
19	18	lt0neg1d	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( ( Im ` A ) < 0 <-> 0 < -u ( Im ` A ) ) )
20	1 19	mpbid	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < -u ( Im ` A ) )
21		imcj	|- ( A e. CC -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
22	21	adantr	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
23	20 22	breqtrrd	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < ( Im ` ( * ` A ) ) )
24		argimgt0	|- ( ( ( * ` A ) e. CC /\ 0 < ( Im ` ( * ` A ) ) ) -> ( Im ` ( log ` ( * ` A ) ) ) e. ( 0 (,) _pi ) )
25	16 23 24	syl2an2r	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) e. ( 0 (,) _pi ) )
26		eliooord	|- ( ( Im ` ( log ` ( * ` A ) ) ) e. ( 0 (,) _pi ) -> ( 0 < ( Im ` ( log ` ( * ` A ) ) ) /\ ( Im ` ( log ` ( * ` A ) ) ) < _pi ) )
27	25 26	syl	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( 0 < ( Im ` ( log ` ( * ` A ) ) ) /\ ( Im ` ( log ` ( * ` A ) ) ) < _pi ) )
28	27	simprd	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) < _pi )
29	15 28	eqbrtrrd	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> -u ( Im ` ( log ` A ) ) < _pi )
30		pire	|- _pi e. RR
31		ltnegcon1	|- ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( -u ( Im ` ( log ` A ) ) < _pi <-> -u _pi < ( Im ` ( log ` A ) ) ) )
32	10 30 31	sylancl	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( -u ( Im ` ( log ` A ) ) < _pi <-> -u _pi < ( Im ` ( log ` A ) ) ) )
33	29 32	mpbid	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> -u _pi < ( Im ` ( log ` A ) ) )
34	27	simpld	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < ( Im ` ( log ` ( * ` A ) ) ) )
35	34 15	breqtrd	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < -u ( Im ` ( log ` A ) ) )
36	10	lt0neg1d	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` A ) ) < 0 <-> 0 < -u ( Im ` ( log ` A ) ) ) )
37	35 36	mpbird	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) < 0 )
38	30	renegcli	|- -u _pi e. RR
39	38	rexri	|- -u _pi e. RR*
40		0xr	|- 0 e. RR*
41		elioo2	|- ( ( -u _pi e. RR* /\ 0 e. RR* ) -> ( ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < 0 ) ) )
42	39 40 41	mp2an	|- ( ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < 0 ) )
43	10 33 37 42	syl3anbrc	|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) )