Proof of Theorem argimgt0
Step | Hyp | Ref
| Expression |
1 | | imcl 13699 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
2 | | gt0ne0 10372 |
. . . . . 6
⊢
(((ℑ‘𝐴)
∈ ℝ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ≠ 0) |
3 | 1, 2 | sylan 487 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘𝐴) ≠
0) |
4 | | fveq2 6103 |
. . . . . . 7
⊢ (𝐴 = 0 → (ℑ‘𝐴) =
(ℑ‘0)) |
5 | | im0 13741 |
. . . . . . 7
⊢
(ℑ‘0) = 0 |
6 | 4, 5 | syl6eq 2660 |
. . . . . 6
⊢ (𝐴 = 0 → (ℑ‘𝐴) = 0) |
7 | 6 | necon3i 2814 |
. . . . 5
⊢
((ℑ‘𝐴)
≠ 0 → 𝐴 ≠
0) |
8 | 3, 7 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
𝐴 ≠ 0) |
9 | | logcl 24119 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
10 | 8, 9 | syldan 486 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(log‘𝐴) ∈
ℂ) |
11 | 10 | imcld 13783 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
12 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘𝐴)) |
13 | | abscl 13866 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
14 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ∈
ℝ) |
15 | 14 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ∈
ℂ) |
16 | 15 | mul01d 10114 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) · 0)
= 0) |
17 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
𝐴 ∈
ℂ) |
18 | | absrpcl 13876 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
19 | 8, 18 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ∈
ℝ+) |
20 | 19 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ≠
0) |
21 | 17, 15, 20 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(𝐴 / (abs‘𝐴)) ∈
ℂ) |
22 | 14, 21 | immul2d 13816 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = ((abs‘𝐴) · (ℑ‘(𝐴 / (abs‘𝐴))))) |
23 | 17, 15, 20 | divcan2d 10682 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) ·
(𝐴 / (abs‘𝐴))) = 𝐴) |
24 | 23 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = (ℑ‘𝐴)) |
25 | 22, 24 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) ·
(ℑ‘(𝐴 /
(abs‘𝐴)))) =
(ℑ‘𝐴)) |
26 | 12, 16, 25 | 3brtr4d 4615 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) · 0)
< ((abs‘𝐴)
· (ℑ‘(𝐴
/ (abs‘𝐴))))) |
27 | | 0re 9919 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
∈ ℝ) |
29 | 21 | imcld 13783 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(𝐴 /
(abs‘𝐴))) ∈
ℝ) |
30 | 28, 29, 19 | ltmul2d 11790 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 < (ℑ‘(𝐴 /
(abs‘𝐴))) ↔
((abs‘𝐴) · 0)
< ((abs‘𝐴)
· (ℑ‘(𝐴
/ (abs‘𝐴)))))) |
31 | 26, 30 | mpbird 246 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘(𝐴 /
(abs‘𝐴)))) |
32 | | efiarg 24157 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i
· (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
33 | 8, 32 | syldan 486 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
34 | 33 | fveq2d 6107 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(exp‘(i · (ℑ‘(log‘𝐴))))) = (ℑ‘(𝐴 / (abs‘𝐴)))) |
35 | 31, 34 | breqtrrd 4611 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘(exp‘(i · (ℑ‘(log‘𝐴)))))) |
36 | | resinval 14704 |
. . . . . 6
⊢
((ℑ‘(log‘𝐴)) ∈ ℝ →
(sin‘(ℑ‘(log‘𝐴))) = (ℑ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) |
37 | 11, 36 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(sin‘(ℑ‘(log‘𝐴))) = (ℑ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) |
38 | 35, 37 | breqtrrd 4611 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (sin‘(ℑ‘(log‘𝐴)))) |
39 | 11 | resincld 14712 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(sin‘(ℑ‘(log‘𝐴))) ∈ ℝ) |
40 | 39 | lt0neg2d 10477 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 < (sin‘(ℑ‘(log‘𝐴))) ↔
-(sin‘(ℑ‘(log‘𝐴))) < 0)) |
41 | 38, 40 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-(sin‘(ℑ‘(log‘𝐴))) < 0) |
42 | | pire 24014 |
. . . . . . . . . . 11
⊢ π
∈ ℝ |
43 | | readdcl 9898 |
. . . . . . . . . . 11
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ)
→ ((ℑ‘(log‘𝐴)) + π) ∈ ℝ) |
44 | 11, 42, 43 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) + π) ∈ ℝ) |
45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ∈ ℝ) |
46 | | df-neg 10148 |
. . . . . . . . . . . 12
⊢ -π =
(0 − π) |
47 | | logimcl 24120 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
48 | 8, 47 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
49 | 48 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-π < (ℑ‘(log‘𝐴))) |
50 | 42 | renegcli 10221 |
. . . . . . . . . . . . . 14
⊢ -π
∈ ℝ |
51 | | ltle 10005 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
52 | 50, 11, 51 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-π ≤ (ℑ‘(log‘𝐴))) |
54 | 46, 53 | syl5eqbrr 4619 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 − π) ≤ (ℑ‘(log‘𝐴))) |
55 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
π ∈ ℝ) |
56 | 28, 55, 11 | lesubaddd 10503 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((0 − π) ≤ (ℑ‘(log‘𝐴)) ↔ 0 ≤
((ℑ‘(log‘𝐴)) + π))) |
57 | 54, 56 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
≤ ((ℑ‘(log‘𝐴)) + π)) |
58 | 57 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) → 0 ≤
((ℑ‘(log‘𝐴)) + π)) |
59 | 11, 28, 55 | leadd1d 10500 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) ≤ 0 ↔
((ℑ‘(log‘𝐴)) + π) ≤ (0 +
π))) |
60 | 59 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ≤ (0 + π)) |
61 | | picn 24015 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
62 | 61 | addid2i 10103 |
. . . . . . . . . 10
⊢ (0 +
π) = π |
63 | 60, 62 | syl6breq 4624 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ≤ π) |
64 | 27, 42 | elicc2i 12110 |
. . . . . . . . 9
⊢
(((ℑ‘(log‘𝐴)) + π) ∈ (0[,]π) ↔
(((ℑ‘(log‘𝐴)) + π) ∈ ℝ ∧ 0 ≤
((ℑ‘(log‘𝐴)) + π) ∧
((ℑ‘(log‘𝐴)) + π) ≤ π)) |
65 | 45, 58, 63, 64 | syl3anbrc 1239 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ∈
(0[,]π)) |
66 | | sinq12ge0 24064 |
. . . . . . . 8
⊢
(((ℑ‘(log‘𝐴)) + π) ∈ (0[,]π) → 0 ≤
(sin‘((ℑ‘(log‘𝐴)) + π))) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) → 0 ≤
(sin‘((ℑ‘(log‘𝐴)) + π))) |
68 | 11 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
69 | | sinppi 24045 |
. . . . . . . . 9
⊢
((ℑ‘(log‘𝐴)) ∈ ℂ →
(sin‘((ℑ‘(log‘𝐴)) + π)) =
-(sin‘(ℑ‘(log‘𝐴)))) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(sin‘((ℑ‘(log‘𝐴)) + π)) =
-(sin‘(ℑ‘(log‘𝐴)))) |
71 | 70 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
(sin‘((ℑ‘(log‘𝐴)) + π)) =
-(sin‘(ℑ‘(log‘𝐴)))) |
72 | 67, 71 | breqtrd 4609 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) → 0 ≤
-(sin‘(ℑ‘(log‘𝐴)))) |
73 | 72 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) ≤ 0 → 0 ≤
-(sin‘(ℑ‘(log‘𝐴))))) |
74 | 73 | con3d 147 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(¬ 0 ≤ -(sin‘(ℑ‘(log‘𝐴))) → ¬
(ℑ‘(log‘𝐴)) ≤ 0)) |
75 | 39 | renegcld 10336 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-(sin‘(ℑ‘(log‘𝐴))) ∈ ℝ) |
76 | | ltnle 9996 |
. . . . 5
⊢
((-(sin‘(ℑ‘(log‘𝐴))) ∈ ℝ ∧ 0 ∈ ℝ)
→ (-(sin‘(ℑ‘(log‘𝐴))) < 0 ↔ ¬ 0 ≤
-(sin‘(ℑ‘(log‘𝐴))))) |
77 | 75, 27, 76 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-(sin‘(ℑ‘(log‘𝐴))) < 0 ↔ ¬ 0 ≤
-(sin‘(ℑ‘(log‘𝐴))))) |
78 | | ltnle 9996 |
. . . . 5
⊢ ((0
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (0 <
(ℑ‘(log‘𝐴)) ↔ ¬
(ℑ‘(log‘𝐴)) ≤ 0)) |
79 | 27, 11, 78 | sylancr 694 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 < (ℑ‘(log‘𝐴)) ↔ ¬
(ℑ‘(log‘𝐴)) ≤ 0)) |
80 | 74, 77, 79 | 3imtr4d 282 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-(sin‘(ℑ‘(log‘𝐴))) < 0 → 0 <
(ℑ‘(log‘𝐴)))) |
81 | 41, 80 | mpd 15 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘(log‘𝐴))) |
82 | | rpre 11715 |
. . . . . . . . 9
⊢ (-𝐴 ∈ ℝ+
→ -𝐴 ∈
ℝ) |
83 | 82 | renegcld 10336 |
. . . . . . . 8
⊢ (-𝐴 ∈ ℝ+
→ --𝐴 ∈
ℝ) |
84 | | negneg 10210 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴) |
85 | 84 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
--𝐴 = 𝐴) |
86 | 85 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(--𝐴 ∈ ℝ ↔
𝐴 ∈
ℝ)) |
87 | 83, 86 | syl5ib 233 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-𝐴 ∈
ℝ+ → 𝐴 ∈ ℝ)) |
88 | | lognegb 24140 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
89 | 8, 88 | syldan 486 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-𝐴 ∈
ℝ+ ↔ (ℑ‘(log‘𝐴)) = π)) |
90 | | reim0b 13707 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
91 | 90 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
92 | 87, 89, 91 | 3imtr3d 281 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) = π → (ℑ‘𝐴) = 0)) |
93 | 92 | necon3d 2803 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘𝐴) ≠ 0
→ (ℑ‘(log‘𝐴)) ≠ π)) |
94 | 3, 93 | mpd 15 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≠ π) |
95 | 94 | necomd 2837 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
π ≠ (ℑ‘(log‘𝐴))) |
96 | 48 | simprd 478 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≤ π) |
97 | 11, 55, 96 | leltned 10069 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) < π ↔ π ≠
(ℑ‘(log‘𝐴)))) |
98 | 95, 97 | mpbird 246 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) < π) |
99 | | 0xr 9965 |
. . 3
⊢ 0 ∈
ℝ* |
100 | 42 | rexri 9976 |
. . 3
⊢ π
∈ ℝ* |
101 | | elioo2 12087 |
. . 3
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝐴)) ∈ (0(,)π) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ 0 <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π))) |
102 | 99, 100, 101 | mp2an 704 |
. 2
⊢
((ℑ‘(log‘𝐴)) ∈ (0(,)π) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ 0 <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π)) |
103 | 11, 81, 98, 102 | syl3anbrc 1239 |
1
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ (0(,)π)) |