Metamath Proof Explorer

Theorem argregt0

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

Ref Expression
Assertion argregt0 ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )

Proof

Step Hyp Ref Expression
1 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
2 gt0ne0 ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ≠ 0 )
3 1 2 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ≠ 0 )
4 fveq2 ⊢ ( 𝐴 = 0 → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ 0 ) )
5 re0 ⊢ ( ℜ ‘ 0 ) = 0
6 4 5 eqtrdi ⊢ ( 𝐴 = 0 → ( ℜ ‘ 𝐴 ) = 0 )
7 6 necon3i ⊢ ( ( ℜ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ 0 )
8 3 7 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 𝐴 ≠ 0 )
9 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
10 8 9 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
11 10 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
12 coshalfpi ⊢ ( cos ‘ ( π / 2 ) ) = 0
13 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ 𝐴 ) )
14 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
16 15 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
17 16 mul01d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) = 0 )
18 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
19 absrpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
20 8 19 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
21 20 rpne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ≠ 0 )
22 18 16 21 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) ∈ ℂ )
23 15 22 remul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) )
24 18 16 21 divcan2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) = 𝐴 )
25 24 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℜ ‘ 𝐴 ) )
26 23 25 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℜ ‘ 𝐴 ) )
27 13 17 26 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) < ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) )
28 0re ⊢ 0 ∈ ℝ
29 28 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 ∈ ℝ )
30 22 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ∈ ℝ )
31 29 30 20 ltmul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 0 < ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ↔ ( ( abs ‘ 𝐴 ) · 0 ) < ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) ) )
32 27 31 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) )
33 efiarg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
34 8 33 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
35 34 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) )
36 32 35 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
37 recosval ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
38 11 37 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
39 36 38 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
40 fveq2 ⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
41 40 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
42 11 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
43 cosneg ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ → ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
44 42 43 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
45 fveqeq2 ⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
46 44 45 syl5ibrcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
47 11 absord ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) ∨ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
48 41 46 47 mpjaod ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
49 39 48 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
50 12 49 eqbrtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( π / 2 ) ) < ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
51 42 abscld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
52 42 absge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
53 logimcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
54 8 53 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
55 54 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
56 pire ⊢ π ∈ ℝ
57 56 renegcli ⊢ - π ∈ ℝ
58 ltle ⊢ ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
59 57 11 58 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
60 55 59 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
61 54 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
62 absle ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) )
63 11 56 62 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) )
64 60 61 63 mpbir2and ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π )
65 28 56 elicc2i ⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ↔ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∧ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ) )
66 51 52 64 65 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) )
67 halfpire ⊢ ( π / 2 ) ∈ ℝ
68 pirp ⊢ π ∈ ℝ+
69 rphalfcl ⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ )
70 rpge0 ⊢ ( ( π / 2 ) ∈ ℝ+ → 0 ≤ ( π / 2 ) )
71 68 69 70 mp2b ⊢ 0 ≤ ( π / 2 )
72 rphalflt ⊢ ( π ∈ ℝ+ → ( π / 2 ) < π )
73 68 72 ax-mp ⊢ ( π / 2 ) < π
74 67 56 73 ltleii ⊢ ( π / 2 ) ≤ π
75 28 56 elicc2i ⊢ ( ( π / 2 ) ∈ ( 0 [,] π ) ↔ ( ( π / 2 ) ∈ ℝ ∧ 0 ≤ ( π / 2 ) ∧ ( π / 2 ) ≤ π ) )
76 67 71 74 75 mpbir3an ⊢ ( π / 2 ) ∈ ( 0 [,] π )
77 cosord ⊢ ( ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ∧ ( π / 2 ) ∈ ( 0 [,] π ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < ( π / 2 ) ↔ ( cos ‘ ( π / 2 ) ) < ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
78 66 76 77 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < ( π / 2 ) ↔ ( cos ‘ ( π / 2 ) ) < ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
79 50 78 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < ( π / 2 ) )
80 abslt ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < ( π / 2 ) ↔ ( - ( π / 2 ) < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( π / 2 ) ) ) )
81 11 67 80 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < ( π / 2 ) ↔ ( - ( π / 2 ) < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( π / 2 ) ) ) )
82 79 81 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - ( π / 2 ) < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( π / 2 ) ) )
83 82 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - ( π / 2 ) < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
84 82 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( π / 2 ) )
85 67 renegcli ⊢ - ( π / 2 ) ∈ ℝ
86 85 rexri ⊢ - ( π / 2 ) ∈ ℝ*
87 67 rexri ⊢ ( π / 2 ) ∈ ℝ*
88 elioo2 ⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( π / 2 ) ) ) )
89 86 87 88 mp2an ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( π / 2 ) ) )
90 11 83 84 89 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )