Metamath Proof Explorer

Theorem argrege0

Description: Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion argrege0 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ − π 2 π 2

Proof

Step Hyp Ref Expression
1 logcl ⊢ A ∈ ℂ ∧ A ≠ 0 → log ⁡ A ∈ ℂ
2 1 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → log ⁡ A ∈ ℂ
3 2 imcld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ ℝ
4 simp3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ≤ ℜ ⁡ A
5 simp1 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ∈ ℂ
6 5 abscld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ∈ ℝ
7 6 recnd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ∈ ℂ
8 7 mul01d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ⋅ 0 = 0
9 absrpcl ⊢ A ∈ ℂ ∧ A ≠ 0 → A ∈ ℝ +
10 9 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ∈ ℝ +
11 10 rpne0d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ≠ 0
12 5 7 11 divcld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A A ∈ ℂ
13 6 12 remul2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℜ ⁡ A ⁢ A A = A ⁢ ℜ ⁡ A A
14 5 7 11 divcan2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ⁢ A A = A
15 14 fveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℜ ⁡ A ⁢ A A = ℜ ⁡ A
16 13 15 eqtr3d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ⁢ ℜ ⁡ A A = ℜ ⁡ A
17 4 8 16 3brtr4d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → A ⋅ 0 ≤ A ⁢ ℜ ⁡ A A
18 0re ⊢ 0 ∈ ℝ
19 18 a1i ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ∈ ℝ
20 12 recld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℜ ⁡ A A ∈ ℝ
21 19 20 10 lemul2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ≤ ℜ ⁡ A A ↔ A ⋅ 0 ≤ A ⁢ ℜ ⁡ A A
22 17 21 mpbird ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ≤ ℜ ⁡ A A
23 efiarg ⊢ A ∈ ℂ ∧ A ≠ 0 → e i ⁢ ℑ ⁡ log ⁡ A = A A
24 23 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → e i ⁢ ℑ ⁡ log ⁡ A = A A
25 24 fveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A = ℜ ⁡ A A
26 22 25 breqtrrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ≤ ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
27 recosval ⊢ ℑ ⁡ log ⁡ A ∈ ℝ → cos ⁡ ℑ ⁡ log ⁡ A = ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
28 3 27 syl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
29 26 28 breqtrrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ≤ cos ⁡ ℑ ⁡ log ⁡ A
30 halfpire ⊢ π 2 ∈ ℝ
31 pirp ⊢ π ∈ ℝ +
32 rphalfcl ⊢ π ∈ ℝ + → π 2 ∈ ℝ +
33 rpge0 ⊢ π 2 ∈ ℝ + → 0 ≤ π 2
34 31 32 33 mp2b ⊢ 0 ≤ π 2
35 pire ⊢ π ∈ ℝ
36 rphalflt ⊢ π ∈ ℝ + → π 2 < π
37 31 36 ax-mp ⊢ π 2 < π
38 30 35 37 ltleii ⊢ π 2 ≤ π
39 18 35 elicc2i ⊢ π 2 ∈ 0 π ↔ π 2 ∈ ℝ ∧ 0 ≤ π 2 ∧ π 2 ≤ π
40 30 34 38 39 mpbir3an ⊢ π 2 ∈ 0 π
41 3 recnd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ ℂ
42 41 abscld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ ℝ
43 41 absge0d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ≤ ℑ ⁡ log ⁡ A
44 logimcl ⊢ A ∈ ℂ ∧ A ≠ 0 → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
45 44 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
46 45 simpld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → − π < ℑ ⁡ log ⁡ A
47 35 renegcli ⊢ − π ∈ ℝ
48 ltle ⊢ − π ∈ ℝ ∧ ℑ ⁡ log ⁡ A ∈ ℝ → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
49 47 3 48 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
50 46 49 mpd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
51 45 simprd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π
52 absle ⊢ ℑ ⁡ log ⁡ A ∈ ℝ ∧ π ∈ ℝ → ℑ ⁡ log ⁡ A ≤ π ↔ − π ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
53 3 35 52 sylancl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π ↔ − π ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
54 50 51 53 mpbir2and ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π
55 18 35 elicc2i ⊢ ℑ ⁡ log ⁡ A ∈ 0 π ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ 0 ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
56 42 43 54 55 syl3anbrc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ 0 π
57 cosord ⊢ π 2 ∈ 0 π ∧ ℑ ⁡ log ⁡ A ∈ 0 π → π 2 < ℑ ⁡ log ⁡ A ↔ cos ⁡ ℑ ⁡ log ⁡ A < cos ⁡ π 2
58 40 56 57 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → π 2 < ℑ ⁡ log ⁡ A ↔ cos ⁡ ℑ ⁡ log ⁡ A < cos ⁡ π 2
59 fveq2 ⊢ ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
60 59 a1i ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
61 cosneg ⊢ ℑ ⁡ log ⁡ A ∈ ℂ → cos ⁡ − ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
62 41 61 syl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → cos ⁡ − ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
63 fveqeq2 ⊢ ℑ ⁡ log ⁡ A = − ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A ↔ cos ⁡ − ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
64 62 63 syl5ibrcom ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A = − ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
65 3 absord ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A ∨ ℑ ⁡ log ⁡ A = − ℑ ⁡ log ⁡ A
66 60 64 65 mpjaod ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
67 coshalfpi ⊢ cos ⁡ π 2 = 0
68 67 a1i ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → cos ⁡ π 2 = 0
69 66 68 breq12d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A < cos ⁡ π 2 ↔ cos ⁡ ℑ ⁡ log ⁡ A < 0
70 58 69 bitrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → π 2 < ℑ ⁡ log ⁡ A ↔ cos ⁡ ℑ ⁡ log ⁡ A < 0
71 70 notbid ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ¬ π 2 < ℑ ⁡ log ⁡ A ↔ ¬ cos ⁡ ℑ ⁡ log ⁡ A < 0
72 lenlt ⊢ ℑ ⁡ log ⁡ A ∈ ℝ ∧ π 2 ∈ ℝ → ℑ ⁡ log ⁡ A ≤ π 2 ↔ ¬ π 2 < ℑ ⁡ log ⁡ A
73 42 30 72 sylancl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π 2 ↔ ¬ π 2 < ℑ ⁡ log ⁡ A
74 3 recoscld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A ∈ ℝ
75 lenlt ⊢ 0 ∈ ℝ ∧ cos ⁡ ℑ ⁡ log ⁡ A ∈ ℝ → 0 ≤ cos ⁡ ℑ ⁡ log ⁡ A ↔ ¬ cos ⁡ ℑ ⁡ log ⁡ A < 0
76 18 74 75 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → 0 ≤ cos ⁡ ℑ ⁡ log ⁡ A ↔ ¬ cos ⁡ ℑ ⁡ log ⁡ A < 0
77 71 73 76 3bitr4d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π 2 ↔ 0 ≤ cos ⁡ ℑ ⁡ log ⁡ A
78 29 77 mpbird ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π 2
79 absle ⊢ ℑ ⁡ log ⁡ A ∈ ℝ ∧ π 2 ∈ ℝ → ℑ ⁡ log ⁡ A ≤ π 2 ↔ − π 2 ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π 2
80 3 30 79 sylancl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π 2 ↔ − π 2 ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π 2
81 78 80 mpbid ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → − π 2 ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π 2
82 81 simpld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → − π 2 ≤ ℑ ⁡ log ⁡ A
83 81 simprd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π 2
84 30 renegcli ⊢ − π 2 ∈ ℝ
85 84 30 elicc2i ⊢ ℑ ⁡ log ⁡ A ∈ − π 2 π 2 ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ − π 2 ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π 2
86 3 82 83 85 syl3anbrc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 0 ≤ ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ − π 2 π 2