Metamath Proof Explorer


Theorem 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 0 < A log A 0 π

Proof

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