Metamath Proof Explorer


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 ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - π (,) 0 ) )

Proof

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