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 ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ − π 2 π 2

Proof

Step Hyp Ref Expression
1 recl ⊢ 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 re0 ⊢ ℜ ⁡ 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 coshalfpi ⊢ cos ⁡ π 2 = 0
13 simpr ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 < ℜ ⁡ A
14 abscl ⊢ A ∈ ℂ → A ∈ ℝ
15 14 adantr ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ∈ ℝ
16 15 recnd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ∈ ℂ
17 16 mul01d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ⋅ 0 = 0
18 simpl ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ∈ ℂ
19 absrpcl ⊢ A ∈ ℂ ∧ A ≠ 0 → A ∈ ℝ +
20 8 19 syldan ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ∈ ℝ +
21 20 rpne0d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ≠ 0
22 18 16 21 divcld ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A A ∈ ℂ
23 15 22 remul2d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℜ ⁡ A ⁢ A A = A ⁢ ℜ ⁡ A A
24 18 16 21 divcan2d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ⁢ A A = A
25 24 fveq2d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℜ ⁡ A ⁢ A A = ℜ ⁡ A
26 23 25 eqtr3d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ⁢ ℜ ⁡ A A = ℜ ⁡ A
27 13 17 26 3brtr4d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → A ⋅ 0 < A ⁢ ℜ ⁡ A A
28 0re ⊢ 0 ∈ ℝ
29 28 a1i ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 ∈ ℝ
30 22 recld ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℜ ⁡ A A ∈ ℝ
31 29 30 20 ltmul2d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 < ℜ ⁡ A A ↔ A ⋅ 0 < A ⁢ ℜ ⁡ A A
32 27 31 mpbird ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 < ℜ ⁡ A A
33 efiarg ⊢ A ∈ ℂ ∧ A ≠ 0 → e i ⁢ ℑ ⁡ log ⁡ A = A A
34 8 33 syldan ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → e i ⁢ ℑ ⁡ log ⁡ A = A A
35 34 fveq2d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A = ℜ ⁡ A A
36 32 35 breqtrrd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 < ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
37 recosval ⊢ ℑ ⁡ log ⁡ A ∈ ℝ → cos ⁡ ℑ ⁡ log ⁡ A = ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
38 11 37 syl ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = ℜ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
39 36 38 breqtrrd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 < cos ⁡ ℑ ⁡ log ⁡ A
40 fveq2 ⊢ ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
41 40 a1i ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
42 11 recnd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ ℂ
43 cosneg ⊢ ℑ ⁡ log ⁡ A ∈ ℂ → cos ⁡ − ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
44 42 43 syl ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → cos ⁡ − ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
45 fveqeq2 ⊢ ℑ ⁡ log ⁡ A = − ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A ↔ cos ⁡ − ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
46 44 45 syl5ibrcom ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A = − ℑ ⁡ log ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
47 11 absord ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A ∨ ℑ ⁡ log ⁡ A = − ℑ ⁡ log ⁡ A
48 41 46 47 mpjaod ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → cos ⁡ ℑ ⁡ log ⁡ A = cos ⁡ ℑ ⁡ log ⁡ A
49 39 48 breqtrrd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 < cos ⁡ ℑ ⁡ log ⁡ A
50 12 49 eqbrtrid ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → cos ⁡ π 2 < cos ⁡ ℑ ⁡ log ⁡ A
51 42 abscld ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ ℝ
52 42 absge0d ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → 0 ≤ ℑ ⁡ log ⁡ A
53 logimcl ⊢ A ∈ ℂ ∧ A ≠ 0 → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
54 8 53 syldan ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
55 54 simpld ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → − π < ℑ ⁡ log ⁡ A
56 pire ⊢ π ∈ ℝ
57 56 renegcli ⊢ − π ∈ ℝ
58 ltle ⊢ − π ∈ ℝ ∧ ℑ ⁡ log ⁡ A ∈ ℝ → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
59 57 11 58 sylancr ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
60 55 59 mpd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
61 54 simprd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π
62 absle ⊢ ℑ ⁡ log ⁡ A ∈ ℝ ∧ π ∈ ℝ → ℑ ⁡ log ⁡ A ≤ π ↔ − π ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
63 11 56 62 sylancl ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π ↔ − π ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
64 60 61 63 mpbir2and ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ≤ π
65 28 56 elicc2i ⊢ ℑ ⁡ log ⁡ A ∈ 0 π ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ 0 ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
66 51 52 64 65 syl3anbrc ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ 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 ⊢ ℑ ⁡ log ⁡ A ∈ 0 π ∧ π 2 ∈ 0 π → ℑ ⁡ log ⁡ A < π 2 ↔ cos ⁡ π 2 < cos ⁡ ℑ ⁡ log ⁡ A
78 66 76 77 sylancl ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A < π 2 ↔ cos ⁡ π 2 < cos ⁡ ℑ ⁡ log ⁡ A
79 50 78 mpbird ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A < π 2
80 abslt ⊢ ℑ ⁡ log ⁡ A ∈ ℝ ∧ π 2 ∈ ℝ → ℑ ⁡ log ⁡ A < π 2 ↔ − π 2 < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A < π 2
81 11 67 80 sylancl ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A < π 2 ↔ − π 2 < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A < π 2
82 79 81 mpbid ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → − π 2 < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A < π 2
83 82 simpld ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → − π 2 < ℑ ⁡ log ⁡ A
84 82 simprd ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A < π 2
85 67 renegcli ⊢ − π 2 ∈ ℝ
86 85 rexri ⊢ − π 2 ∈ ℝ *
87 67 rexri ⊢ π 2 ∈ ℝ *
88 elioo2 ⊢ − π 2 ∈ ℝ * ∧ π 2 ∈ ℝ * → ℑ ⁡ log ⁡ A ∈ − π 2 π 2 ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ − π 2 < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A < π 2
89 86 87 88 mp2an ⊢ ℑ ⁡ log ⁡ A ∈ − π 2 π 2 ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ − π 2 < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A < π 2
90 11 83 84 89 syl3anbrc ⊢ A ∈ ℂ ∧ 0 < ℜ ⁡ A → ℑ ⁡ log ⁡ A ∈ − π 2 π 2