argimgt0

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

		Ref	Expression
	Assertion	argimgt0	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) )

Proof

Step	Hyp	Ref	Expression
1		imcl	\|- ( A e. CC -> ( Im ` A ) e. RR )
2		gt0ne0	\|- ( ( ( Im ` A ) e. RR /\ 0 < ( Im ` A ) ) -> ( Im ` A ) =/= 0 )
3	1 2	sylan	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` A ) =/= 0 )
4		fveq2	\|- ( A = 0 -> ( Im ` A ) = ( Im ` 0 ) )
5		im0	\|- ( Im ` 0 ) = 0
6	4 5	eqtrdi	\|- ( A = 0 -> ( Im ` A ) = 0 )
7	6	necon3i	\|- ( ( Im ` A ) =/= 0 -> A =/= 0 )
8	3 7	syl	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> A =/= 0 )
9		logcl	\|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
10	8 9	syldan	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( log ` A ) e. CC )
11	10	imcld	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. RR )
12		simpr	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` A ) )
13		abscl	\|- ( A e. CC -> ( abs ` A ) e. RR )
14	13	adantr	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( abs ` A ) e. RR )
15	14	recnd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( abs ` A ) e. CC )
16	15	mul01d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( abs ` A ) x. 0 ) = 0 )
17		simpl	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> A e. CC )
18		absrpcl	\|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
19	8 18	syldan	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( abs ` A ) e. RR+ )
20	19	rpne0d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( abs ` A ) =/= 0 )
21	17 15 20	divcld	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( A / ( abs ` A ) ) e. CC )
22	14 21	immul2d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( ( abs ` A ) x. ( A / ( abs ` A ) ) ) ) = ( ( abs ` A ) x. ( Im ` ( A / ( abs ` A ) ) ) ) )
23	17 15 20	divcan2d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( abs ` A ) x. ( A / ( abs ` A ) ) ) = A )
24	23	fveq2d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( ( abs ` A ) x. ( A / ( abs ` A ) ) ) ) = ( Im ` A ) )
25	22 24	eqtr3d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( abs ` A ) x. ( Im ` ( A / ( abs ` A ) ) ) ) = ( Im ` A ) )
26	12 16 25	3brtr4d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( abs ` A ) x. 0 ) < ( ( abs ` A ) x. ( Im ` ( A / ( abs ` A ) ) ) ) )
27		0re	\|- 0 e. RR
28	27	a1i	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 e. RR )
29	21	imcld	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( A / ( abs ` A ) ) ) e. RR )
30	28 29 19	ltmul2d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` ( A / ( abs ` A ) ) ) <-> ( ( abs ` A ) x. 0 ) < ( ( abs ` A ) x. ( Im ` ( A / ( abs ` A ) ) ) ) ) )
31	26 30	mpbird	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` ( A / ( abs ` A ) ) ) )
32		efiarg	\|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
33	8 32	syldan	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
34	33	fveq2d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) = ( Im ` ( A / ( abs ` A ) ) ) )
35	31 34	breqtrrd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
36		resinval	\|- ( ( Im ` ( log ` A ) ) e. RR -> ( sin ` ( Im ` ( log ` A ) ) ) = ( Im ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
37	11 36	syl	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( sin ` ( Im ` ( log ` A ) ) ) = ( Im ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
38	35 37	breqtrrd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 < ( sin ` ( Im ` ( log ` A ) ) ) )
39	11	resincld	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( sin ` ( Im ` ( log ` A ) ) ) e. RR )
40	39	lt0neg2d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( 0 < ( sin ` ( Im ` ( log ` A ) ) ) <-> -u ( sin ` ( Im ` ( log ` A ) ) ) < 0 ) )
41	38 40	mpbid	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u ( sin ` ( Im ` ( log ` A ) ) ) < 0 )
42		pire	\|- _pi e. RR
43		readdcl	\|- ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( ( Im ` ( log ` A ) ) + _pi ) e. RR )
44	11 42 43	sylancl	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) + _pi ) e. RR )
45	44	adantr	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> ( ( Im ` ( log ` A ) ) + _pi ) e. RR )
46		df-neg	\|- -u _pi = ( 0 - _pi )
47		logimcl	\|- ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
48	8 47	syldan	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
49	48	simpld	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u _pi < ( Im ` ( log ` A ) ) )
50	42	renegcli	\|- -u _pi e. RR
51		ltle	\|- ( ( -u _pi e. RR /\ ( Im ` ( log ` A ) ) e. RR ) -> ( -u _pi < ( Im ` ( log ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) ) )
52	50 11 51	sylancr	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u _pi < ( Im ` ( log ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) ) )
53	49 52	mpd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) )
54	46 53	eqbrtrrid	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( 0 - _pi ) <_ ( Im ` ( log ` A ) ) )
55	42	a1i	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> _pi e. RR )
56	28 55 11	lesubaddd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( 0 - _pi ) <_ ( Im ` ( log ` A ) ) <-> 0 <_ ( ( Im ` ( log ` A ) ) + _pi ) ) )
57	54 56	mpbid	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 <_ ( ( Im ` ( log ` A ) ) + _pi ) )
58	57	adantr	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> 0 <_ ( ( Im ` ( log ` A ) ) + _pi ) )
59	11 28 55	leadd1d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) <_ 0 <-> ( ( Im ` ( log ` A ) ) + _pi ) <_ ( 0 + _pi ) ) )
60	59	biimpa	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> ( ( Im ` ( log ` A ) ) + _pi ) <_ ( 0 + _pi ) )
61		picn	\|- _pi e. CC
62	61	addlidi	\|- ( 0 + _pi ) = _pi
63	60 62	breqtrdi	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> ( ( Im ` ( log ` A ) ) + _pi ) <_ _pi )
64	27 42	elicc2i	\|- ( ( ( Im ` ( log ` A ) ) + _pi ) e. ( 0 [,] _pi ) <-> ( ( ( Im ` ( log ` A ) ) + _pi ) e. RR /\ 0 <_ ( ( Im ` ( log ` A ) ) + _pi ) /\ ( ( Im ` ( log ` A ) ) + _pi ) <_ _pi ) )
65	45 58 63 64	syl3anbrc	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> ( ( Im ` ( log ` A ) ) + _pi ) e. ( 0 [,] _pi ) )
66		sinq12ge0	\|- ( ( ( Im ` ( log ` A ) ) + _pi ) e. ( 0 [,] _pi ) -> 0 <_ ( sin ` ( ( Im ` ( log ` A ) ) + _pi ) ) )
67	65 66	syl	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> 0 <_ ( sin ` ( ( Im ` ( log ` A ) ) + _pi ) ) )
68	11	recnd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. CC )
69		sinppi	\|- ( ( Im ` ( log ` A ) ) e. CC -> ( sin ` ( ( Im ` ( log ` A ) ) + _pi ) ) = -u ( sin ` ( Im ` ( log ` A ) ) ) )
70	68 69	syl	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( sin ` ( ( Im ` ( log ` A ) ) + _pi ) ) = -u ( sin ` ( Im ` ( log ` A ) ) ) )
71	70	adantr	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> ( sin ` ( ( Im ` ( log ` A ) ) + _pi ) ) = -u ( sin ` ( Im ` ( log ` A ) ) ) )
72	67 71	breqtrd	\|- ( ( ( A e. CC /\ 0 < ( Im ` A ) ) /\ ( Im ` ( log ` A ) ) <_ 0 ) -> 0 <_ -u ( sin ` ( Im ` ( log ` A ) ) ) )
73	72	ex	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) <_ 0 -> 0 <_ -u ( sin ` ( Im ` ( log ` A ) ) ) ) )
74	73	con3d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -. 0 <_ -u ( sin ` ( Im ` ( log ` A ) ) ) -> -. ( Im ` ( log ` A ) ) <_ 0 ) )
75	39	renegcld	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u ( sin ` ( Im ` ( log ` A ) ) ) e. RR )
76		ltnle	\|- ( ( -u ( sin ` ( Im ` ( log ` A ) ) ) e. RR /\ 0 e. RR ) -> ( -u ( sin ` ( Im ` ( log ` A ) ) ) < 0 <-> -. 0 <_ -u ( sin ` ( Im ` ( log ` A ) ) ) ) )
77	75 27 76	sylancl	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u ( sin ` ( Im ` ( log ` A ) ) ) < 0 <-> -. 0 <_ -u ( sin ` ( Im ` ( log ` A ) ) ) ) )
78		ltnle	\|- ( ( 0 e. RR /\ ( Im ` ( log ` A ) ) e. RR ) -> ( 0 < ( Im ` ( log ` A ) ) <-> -. ( Im ` ( log ` A ) ) <_ 0 ) )
79	27 11 78	sylancr	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` ( log ` A ) ) <-> -. ( Im ` ( log ` A ) ) <_ 0 ) )
80	74 77 79	3imtr4d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u ( sin ` ( Im ` ( log ` A ) ) ) < 0 -> 0 < ( Im ` ( log ` A ) ) ) )
81	41 80	mpd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` ( log ` A ) ) )
82	48	simprd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) <_ _pi )
83		rpre	\|- ( -u A e. RR+ -> -u A e. RR )
84	83	renegcld	\|- ( -u A e. RR+ -> -u -u A e. RR )
85		negneg	\|- ( A e. CC -> -u -u A = A )
86	85	adantr	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u -u A = A )
87	86	eleq1d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u -u A e. RR <-> A e. RR ) )
88	84 87	imbitrid	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u A e. RR+ -> A e. RR ) )
89		lognegb	\|- ( ( A e. CC /\ A =/= 0 ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = _pi ) )
90	8 89	syldan	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = _pi ) )
91		reim0b	\|- ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
92	91	adantr	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( A e. RR <-> ( Im ` A ) = 0 ) )
93	88 90 92	3imtr3d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) = _pi -> ( Im ` A ) = 0 ) )
94	93	necon3d	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` A ) =/= 0 -> ( Im ` ( log ` A ) ) =/= _pi ) )
95	3 94	mpd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) =/= _pi )
96	95	necomd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> _pi =/= ( Im ` ( log ` A ) ) )
97	11 55 82 96	leneltd	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) < _pi )
98		0xr	\|- 0 e. RR*
99	42	rexri	\|- _pi e. RR*
100		elioo2	\|- ( ( 0 e. RR* /\ _pi e. RR* ) -> ( ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ 0 < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < _pi ) ) )
101	98 99 100	mp2an	\|- ( ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ 0 < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < _pi ) )
102	11 81 97 101	syl3anbrc	\|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) )

Metamath Proof Explorer

Theorem argimgt0

Proof