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→AA∈ℂ
22 14 21 immul2d ⊢A∈ℂ∧0<ℑ⁡A→ℑ⁡A⁢AA=A⁢ℑ⁡AA
23 17 15 20 divcan2d ⊢A∈ℂ∧0<ℑ⁡A→A⁢AA=A
24 23 fveq2d ⊢A∈ℂ∧0<ℑ⁡A→ℑ⁡A⁢AA=ℑ⁡A
25 22 24 eqtr3d ⊢A∈ℂ∧0<ℑ⁡A→A⁢ℑ⁡AA=ℑ⁡A
26 12 16 25 3brtr4d ⊢A∈ℂ∧0<ℑ⁡A→A⋅0<A⁢ℑ⁡AA
27 0re ⊢0∈ℝ
28 27 a1i ⊢A∈ℂ∧0<ℑ⁡A→0∈ℝ
29 21 imcld ⊢A∈ℂ∧0<ℑ⁡A→ℑ⁡AA∈ℝ
30 28 29 19 ltmul2d ⊢A∈ℂ∧0<ℑ⁡A→0<ℑ⁡AA↔A⋅0<A⁢ℑ⁡AA
31 26 30 mpbird ⊢A∈ℂ∧0<ℑ⁡A→0<ℑ⁡AA
32 efiarg ⊢A∈ℂ∧A≠0→ei⁢ℑ⁡log⁡A=AA
33 8 32 syldan ⊢A∈ℂ∧0<ℑ⁡A→ei⁢ℑ⁡log⁡A=AA
34 33 fveq2d ⊢A∈ℂ∧0<ℑ⁡A→ℑ⁡ei⁢ℑ⁡log⁡A=ℑ⁡AA
35 31 34 breqtrrd ⊢A∈ℂ∧0<ℑ⁡A→0<ℑ⁡ei⁢ℑ⁡log⁡A
36 resinval ⊢ℑ⁡log⁡A∈ℝ→sin⁡ℑ⁡log⁡A=ℑ⁡ei⁢ℑ⁡log⁡A
37 11 36 syl ⊢A∈ℂ∧0<ℑ⁡A→sin⁡ℑ⁡log⁡A=ℑ⁡ei⁢ℑ⁡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 addlidi ⊢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 imbitrid ⊢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π