Metamath Proof Explorer

Theorem argimgt0

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

Ref Expression
Assertion argimgt0 ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A ∈ 0 π

Proof

Step Hyp Ref Expression
1 imcl ⊢ 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 im0 ⊢ ℑ ⁡ 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 simpr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < ℑ ⁡ A
13 abscl ⊢ A ∈ ℂ → A ∈ ℝ
14 13 adantr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ∈ ℝ
15 14 recnd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ∈ ℂ
16 15 mul01d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ⋅ 0 = 0
17 simpl ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ∈ ℂ
18 absrpcl ⊢ A ∈ ℂ ∧ A ≠ 0 → A ∈ ℝ +
19 8 18 syldan ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ∈ ℝ +
20 19 rpne0d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ≠ 0
21 17 15 20 divcld ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A A ∈ ℂ
22 14 21 immul2d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ A ⁢ A A = A ⁢ ℑ ⁡ A A
23 17 15 20 divcan2d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ⁢ A A = A
24 23 fveq2d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ A ⁢ A A = ℑ ⁡ A
25 22 24 eqtr3d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ⁢ ℑ ⁡ A A = ℑ ⁡ A
26 12 16 25 3brtr4d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ⋅ 0 < A ⁢ ℑ ⁡ A A
27 0re ⊢ 0 ∈ ℝ
28 27 a1i ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 ∈ ℝ
29 21 imcld ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ A A ∈ ℝ
30 28 29 19 ltmul2d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < ℑ ⁡ A A ↔ A ⋅ 0 < A ⁢ ℑ ⁡ A A
31 26 30 mpbird ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < ℑ ⁡ A A
32 efiarg ⊢ A ∈ ℂ ∧ A ≠ 0 → e i ⁢ ℑ ⁡ log ⁡ A = A A
33 8 32 syldan ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → e i ⁢ ℑ ⁡ log ⁡ A = A A
34 33 fveq2d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ e i ⁢ ℑ ⁡ log ⁡ A = ℑ ⁡ A A
35 31 34 breqtrrd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < ℑ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
36 resinval ⊢ ℑ ⁡ log ⁡ A ∈ ℝ → sin ⁡ ℑ ⁡ log ⁡ A = ℑ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
37 11 36 syl ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → sin ⁡ ℑ ⁡ log ⁡ A = ℑ ⁡ e i ⁢ ℑ ⁡ log ⁡ A
38 35 37 breqtrrd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < sin ⁡ ℑ ⁡ log ⁡ A
39 11 resincld ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → sin ⁡ ℑ ⁡ log ⁡ A ∈ ℝ
40 39 lt0neg2d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < sin ⁡ ℑ ⁡ log ⁡ A ↔ − sin ⁡ ℑ ⁡ log ⁡ A < 0
41 38 40 mpbid ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − sin ⁡ ℑ ⁡ log ⁡ A < 0
42 pire ⊢ π ∈ ℝ
43 readdcl ⊢ ℑ ⁡ log ⁡ A ∈ ℝ ∧ π ∈ ℝ → ℑ ⁡ log ⁡ A + π ∈ ℝ
44 11 42 43 sylancl ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A + π ∈ ℝ
45 44 adantr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → ℑ ⁡ log ⁡ A + π ∈ ℝ
46 df-neg ⊢ − π = 0 − π
47 logimcl ⊢ A ∈ ℂ ∧ A ≠ 0 → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
48 8 47 syldan ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
49 48 simpld ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − π < ℑ ⁡ log ⁡ A
50 42 renegcli ⊢ − π ∈ ℝ
51 ltle ⊢ − π ∈ ℝ ∧ ℑ ⁡ log ⁡ A ∈ ℝ → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
52 50 11 51 sylancr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
53 49 52 mpd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
54 46 53 eqbrtrrid ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 − π ≤ ℑ ⁡ log ⁡ A
55 42 a1i ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → π ∈ ℝ
56 28 55 11 lesubaddd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 − π ≤ ℑ ⁡ log ⁡ A ↔ 0 ≤ ℑ ⁡ log ⁡ A + π
57 54 56 mpbid ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 ≤ ℑ ⁡ log ⁡ A + π
58 57 adantr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → 0 ≤ ℑ ⁡ log ⁡ A + π
59 11 28 55 leadd1d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A ≤ 0 ↔ ℑ ⁡ log ⁡ A + π ≤ 0 + π
60 59 biimpa ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → ℑ ⁡ log ⁡ A + π ≤ 0 + π
61 picn ⊢ π ∈ ℂ
62 61 addlidi ⊢ 0 + π = π
63 60 62 breqtrdi ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → ℑ ⁡ log ⁡ A + π ≤ π
64 27 42 elicc2i ⊢ ℑ ⁡ log ⁡ A + π ∈ 0 π ↔ ℑ ⁡ log ⁡ A + π ∈ ℝ ∧ 0 ≤ ℑ ⁡ log ⁡ A + π ∧ ℑ ⁡ log ⁡ A + π ≤ π
65 45 58 63 64 syl3anbrc ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → ℑ ⁡ log ⁡ A + π ∈ 0 π
66 sinq12ge0 ⊢ ℑ ⁡ log ⁡ A + π ∈ 0 π → 0 ≤ sin ⁡ ℑ ⁡ log ⁡ A + π
67 65 66 syl ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → 0 ≤ sin ⁡ ℑ ⁡ log ⁡ A + π
68 11 recnd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A ∈ ℂ
69 sinppi ⊢ ℑ ⁡ log ⁡ A ∈ ℂ → sin ⁡ ℑ ⁡ log ⁡ A + π = − sin ⁡ ℑ ⁡ log ⁡ A
70 68 69 syl ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → sin ⁡ ℑ ⁡ log ⁡ A + π = − sin ⁡ ℑ ⁡ log ⁡ A
71 70 adantr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → sin ⁡ ℑ ⁡ log ⁡ A + π = − sin ⁡ ℑ ⁡ log ⁡ A
72 67 71 breqtrd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ 0 → 0 ≤ − sin ⁡ ℑ ⁡ log ⁡ A
73 72 ex ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A ≤ 0 → 0 ≤ − sin ⁡ ℑ ⁡ log ⁡ A
74 73 con3d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ¬ 0 ≤ − sin ⁡ ℑ ⁡ log ⁡ A → ¬ ℑ ⁡ log ⁡ A ≤ 0
75 39 renegcld ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − sin ⁡ ℑ ⁡ log ⁡ A ∈ ℝ
76 ltnle ⊢ − sin ⁡ ℑ ⁡ log ⁡ A ∈ ℝ ∧ 0 ∈ ℝ → − sin ⁡ ℑ ⁡ log ⁡ A < 0 ↔ ¬ 0 ≤ − sin ⁡ ℑ ⁡ log ⁡ A
77 75 27 76 sylancl ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − sin ⁡ ℑ ⁡ log ⁡ A < 0 ↔ ¬ 0 ≤ − sin ⁡ ℑ ⁡ log ⁡ A
78 ltnle ⊢ 0 ∈ ℝ ∧ ℑ ⁡ log ⁡ A ∈ ℝ → 0 < ℑ ⁡ log ⁡ A ↔ ¬ ℑ ⁡ log ⁡ A ≤ 0
79 27 11 78 sylancr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < ℑ ⁡ log ⁡ A ↔ ¬ ℑ ⁡ log ⁡ A ≤ 0
80 74 77 79 3imtr4d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − sin ⁡ ℑ ⁡ log ⁡ A < 0 → 0 < ℑ ⁡ log ⁡ A
81 41 80 mpd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → 0 < ℑ ⁡ log ⁡ A
82 48 simprd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A ≤ π
83 rpre ⊢ − A ∈ ℝ + → − A ∈ ℝ
84 83 renegcld ⊢ − A ∈ ℝ + → − − A ∈ ℝ
85 negneg ⊢ A ∈ ℂ → − − A = A
86 85 adantr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − − A = A
87 86 eleq1d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − − A ∈ ℝ ↔ A ∈ ℝ
88 84 87 imbitrid ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − A ∈ ℝ + → A ∈ ℝ
89 lognegb ⊢ A ∈ ℂ ∧ A ≠ 0 → − A ∈ ℝ + ↔ ℑ ⁡ log ⁡ A = π
90 8 89 syldan ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → − A ∈ ℝ + ↔ ℑ ⁡ log ⁡ A = π
91 reim0b ⊢ A ∈ ℂ → A ∈ ℝ ↔ ℑ ⁡ A = 0
92 91 adantr ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → A ∈ ℝ ↔ ℑ ⁡ A = 0
93 88 90 92 3imtr3d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A = π → ℑ ⁡ A = 0
94 93 necon3d ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ A ≠ 0 → ℑ ⁡ log ⁡ A ≠ π
95 3 94 mpd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A ≠ π
96 95 necomd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → π ≠ ℑ ⁡ log ⁡ A
97 11 55 82 96 leneltd ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A < π
98 0xr ⊢ 0 ∈ ℝ *
99 42 rexri ⊢ π ∈ ℝ *
100 elioo2 ⊢ 0 ∈ ℝ * ∧ π ∈ ℝ * → ℑ ⁡ log ⁡ A ∈ 0 π ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ 0 < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A < π
101 98 99 100 mp2an ⊢ ℑ ⁡ log ⁡ A ∈ 0 π ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ 0 < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A < π
102 11 81 97 101 syl3anbrc ⊢ A ∈ ℂ ∧ 0 < ℑ ⁡ A → ℑ ⁡ log ⁡ A ∈ 0 π