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 ) )