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→AA∈ℂ
23 15 22 remul2d ⊢A∈ℂ∧0<ℜ⁡A→ℜ⁡A⁢AA=A⁢ℜ⁡AA
24 18 16 21 divcan2d ⊢A∈ℂ∧0<ℜ⁡A→A⁢AA=A
25 24 fveq2d ⊢A∈ℂ∧0<ℜ⁡A→ℜ⁡A⁢AA=ℜ⁡A
26 23 25 eqtr3d ⊢A∈ℂ∧0<ℜ⁡A→A⁢ℜ⁡AA=ℜ⁡A
27 13 17 26 3brtr4d ⊢A∈ℂ∧0<ℜ⁡A→A⋅0<A⁢ℜ⁡AA
28 0re ⊢0∈ℝ
29 28 a1i ⊢A∈ℂ∧0<ℜ⁡A→0∈ℝ
30 22 recld ⊢A∈ℂ∧0<ℜ⁡A→ℜ⁡AA∈ℝ
31 29 30 20 ltmul2d ⊢A∈ℂ∧0<ℜ⁡A→0<ℜ⁡AA↔A⋅0<A⁢ℜ⁡AA
32 27 31 mpbird ⊢A∈ℂ∧0<ℜ⁡A→0<ℜ⁡AA
33 efiarg ⊢A∈ℂ∧A≠0→ei⁢ℑ⁡log⁡A=AA
34 8 33 syldan ⊢A∈ℂ∧0<ℜ⁡A→ei⁢ℑ⁡log⁡A=AA
35 34 fveq2d ⊢A∈ℂ∧0<ℜ⁡A→ℜ⁡ei⁢ℑ⁡log⁡A=ℜ⁡AA
36 32 35 breqtrrd ⊢A∈ℂ∧0<ℜ⁡A→0<ℜ⁡ei⁢ℑ⁡log⁡A
37 recosval ⊢ℑ⁡log⁡A∈ℝ→cos⁡ℑ⁡log⁡A=ℜ⁡ei⁢ℑ⁡log⁡A
38 11 37 syl ⊢A∈ℂ∧0<ℜ⁡A→cos⁡ℑ⁡log⁡A=ℜ⁡ei⁢ℑ⁡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