Proof of Theorem argimgt0
Step | Hyp | Ref
| Expression |
1 | | imcl 13851 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
2 | | gt0ne0 10493 |
. . . . . 6
⊢
(((ℑ‘𝐴)
∈ ℝ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ≠ 0) |
3 | 1, 2 | sylan 488 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘𝐴) ≠
0) |
4 | | fveq2 6191 |
. . . . . . 7
⊢ (𝐴 = 0 → (ℑ‘𝐴) =
(ℑ‘0)) |
5 | | im0 13893 |
. . . . . . 7
⊢
(ℑ‘0) = 0 |
6 | 4, 5 | syl6eq 2672 |
. . . . . 6
⊢ (𝐴 = 0 → (ℑ‘𝐴) = 0) |
7 | 6 | necon3i 2826 |
. . . . 5
⊢
((ℑ‘𝐴)
≠ 0 → 𝐴 ≠
0) |
8 | 3, 7 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
𝐴 ≠ 0) |
9 | | logcl 24315 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
10 | 8, 9 | syldan 487 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(log‘𝐴) ∈
ℂ) |
11 | 10 | imcld 13935 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
12 | | simpr 477 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘𝐴)) |
13 | | abscl 14018 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
14 | 13 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ∈
ℝ) |
15 | 14 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ∈
ℂ) |
16 | 15 | mul01d 10235 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) · 0)
= 0) |
17 | | simpl 473 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
𝐴 ∈
ℂ) |
18 | | absrpcl 14028 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
19 | 8, 18 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ∈
ℝ+) |
20 | 19 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(abs‘𝐴) ≠
0) |
21 | 17, 15, 20 | divcld 10801 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(𝐴 / (abs‘𝐴)) ∈
ℂ) |
22 | 14, 21 | immul2d 13968 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = ((abs‘𝐴) · (ℑ‘(𝐴 / (abs‘𝐴))))) |
23 | 17, 15, 20 | divcan2d 10803 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) ·
(𝐴 / (abs‘𝐴))) = 𝐴) |
24 | 23 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = (ℑ‘𝐴)) |
25 | 22, 24 | eqtr3d 2658 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) ·
(ℑ‘(𝐴 /
(abs‘𝐴)))) =
(ℑ‘𝐴)) |
26 | 12, 16, 25 | 3brtr4d 4685 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((abs‘𝐴) · 0)
< ((abs‘𝐴)
· (ℑ‘(𝐴
/ (abs‘𝐴))))) |
27 | | 0re 10040 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
∈ ℝ) |
29 | 21 | imcld 13935 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(𝐴 /
(abs‘𝐴))) ∈
ℝ) |
30 | 28, 29, 19 | ltmul2d 11914 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 < (ℑ‘(𝐴 /
(abs‘𝐴))) ↔
((abs‘𝐴) · 0)
< ((abs‘𝐴)
· (ℑ‘(𝐴
/ (abs‘𝐴)))))) |
31 | 26, 30 | mpbird 247 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘(𝐴 /
(abs‘𝐴)))) |
32 | | efiarg 24353 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i
· (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
33 | 8, 32 | syldan 487 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
34 | 33 | fveq2d 6195 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(exp‘(i · (ℑ‘(log‘𝐴))))) = (ℑ‘(𝐴 / (abs‘𝐴)))) |
35 | 31, 34 | breqtrrd 4681 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘(exp‘(i · (ℑ‘(log‘𝐴)))))) |
36 | | resinval 14865 |
. . . . . 6
⊢
((ℑ‘(log‘𝐴)) ∈ ℝ →
(sin‘(ℑ‘(log‘𝐴))) = (ℑ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) |
37 | 11, 36 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(sin‘(ℑ‘(log‘𝐴))) = (ℑ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) |
38 | 35, 37 | breqtrrd 4681 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (sin‘(ℑ‘(log‘𝐴)))) |
39 | 11 | resincld 14873 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(sin‘(ℑ‘(log‘𝐴))) ∈ ℝ) |
40 | 39 | lt0neg2d 10598 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 < (sin‘(ℑ‘(log‘𝐴))) ↔
-(sin‘(ℑ‘(log‘𝐴))) < 0)) |
41 | 38, 40 | mpbid 222 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-(sin‘(ℑ‘(log‘𝐴))) < 0) |
42 | | pire 24210 |
. . . . . . . . . . 11
⊢ π
∈ ℝ |
43 | | readdcl 10019 |
. . . . . . . . . . 11
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ)
→ ((ℑ‘(log‘𝐴)) + π) ∈ ℝ) |
44 | 11, 42, 43 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) + π) ∈ ℝ) |
45 | 44 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ∈ ℝ) |
46 | | df-neg 10269 |
. . . . . . . . . . . 12
⊢ -π =
(0 − π) |
47 | | logimcl 24316 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
48 | 8, 47 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
49 | 48 | simpld 475 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-π < (ℑ‘(log‘𝐴))) |
50 | 42 | renegcli 10342 |
. . . . . . . . . . . . . 14
⊢ -π
∈ ℝ |
51 | | ltle 10126 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
52 | 50, 11, 51 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-π ≤ (ℑ‘(log‘𝐴))) |
54 | 46, 53 | syl5eqbrr 4689 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 − π) ≤ (ℑ‘(log‘𝐴))) |
55 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
π ∈ ℝ) |
56 | 28, 55, 11 | lesubaddd 10624 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((0 − π) ≤ (ℑ‘(log‘𝐴)) ↔ 0 ≤
((ℑ‘(log‘𝐴)) + π))) |
57 | 54, 56 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
≤ ((ℑ‘(log‘𝐴)) + π)) |
58 | 57 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) → 0 ≤
((ℑ‘(log‘𝐴)) + π)) |
59 | 11, 28, 55 | leadd1d 10621 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) ≤ 0 ↔
((ℑ‘(log‘𝐴)) + π) ≤ (0 +
π))) |
60 | 59 | biimpa 501 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ≤ (0 + π)) |
61 | | picn 24211 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
62 | 61 | addid2i 10224 |
. . . . . . . . . 10
⊢ (0 +
π) = π |
63 | 60, 62 | syl6breq 4694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ≤ π) |
64 | 27, 42 | elicc2i 12239 |
. . . . . . . . 9
⊢
(((ℑ‘(log‘𝐴)) + π) ∈ (0[,]π) ↔
(((ℑ‘(log‘𝐴)) + π) ∈ ℝ ∧ 0 ≤
((ℑ‘(log‘𝐴)) + π) ∧
((ℑ‘(log‘𝐴)) + π) ≤ π)) |
65 | 45, 58, 63, 64 | syl3anbrc 1246 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
((ℑ‘(log‘𝐴)) + π) ∈
(0[,]π)) |
66 | | sinq12ge0 24260 |
. . . . . . . 8
⊢
(((ℑ‘(log‘𝐴)) + π) ∈ (0[,]π) → 0 ≤
(sin‘((ℑ‘(log‘𝐴)) + π))) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) → 0 ≤
(sin‘((ℑ‘(log‘𝐴)) + π))) |
68 | 11 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
69 | | sinppi 24241 |
. . . . . . . . 9
⊢
((ℑ‘(log‘𝐴)) ∈ ℂ →
(sin‘((ℑ‘(log‘𝐴)) + π)) =
-(sin‘(ℑ‘(log‘𝐴)))) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(sin‘((ℑ‘(log‘𝐴)) + π)) =
-(sin‘(ℑ‘(log‘𝐴)))) |
71 | 70 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) →
(sin‘((ℑ‘(log‘𝐴)) + π)) =
-(sin‘(ℑ‘(log‘𝐴)))) |
72 | 67, 71 | breqtrd 4679 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) ∧
(ℑ‘(log‘𝐴)) ≤ 0) → 0 ≤
-(sin‘(ℑ‘(log‘𝐴)))) |
73 | 72 | ex 450 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) ≤ 0 → 0 ≤
-(sin‘(ℑ‘(log‘𝐴))))) |
74 | 73 | con3d 148 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(¬ 0 ≤ -(sin‘(ℑ‘(log‘𝐴))) → ¬
(ℑ‘(log‘𝐴)) ≤ 0)) |
75 | 39 | renegcld 10457 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
-(sin‘(ℑ‘(log‘𝐴))) ∈ ℝ) |
76 | | ltnle 10117 |
. . . . 5
⊢
((-(sin‘(ℑ‘(log‘𝐴))) ∈ ℝ ∧ 0 ∈ ℝ)
→ (-(sin‘(ℑ‘(log‘𝐴))) < 0 ↔ ¬ 0 ≤
-(sin‘(ℑ‘(log‘𝐴))))) |
77 | 75, 27, 76 | sylancl 694 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-(sin‘(ℑ‘(log‘𝐴))) < 0 ↔ ¬ 0 ≤
-(sin‘(ℑ‘(log‘𝐴))))) |
78 | | ltnle 10117 |
. . . . 5
⊢ ((0
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (0 <
(ℑ‘(log‘𝐴)) ↔ ¬
(ℑ‘(log‘𝐴)) ≤ 0)) |
79 | 27, 11, 78 | sylancr 695 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(0 < (ℑ‘(log‘𝐴)) ↔ ¬
(ℑ‘(log‘𝐴)) ≤ 0)) |
80 | 74, 77, 79 | 3imtr4d 283 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-(sin‘(ℑ‘(log‘𝐴))) < 0 → 0 <
(ℑ‘(log‘𝐴)))) |
81 | 41, 80 | mpd 15 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) → 0
< (ℑ‘(log‘𝐴))) |
82 | | rpre 11839 |
. . . . . . . . 9
⊢ (-𝐴 ∈ ℝ+
→ -𝐴 ∈
ℝ) |
83 | 82 | renegcld 10457 |
. . . . . . . 8
⊢ (-𝐴 ∈ ℝ+
→ --𝐴 ∈
ℝ) |
84 | | negneg 10331 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴) |
85 | 84 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
--𝐴 = 𝐴) |
86 | 85 | eleq1d 2686 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(--𝐴 ∈ ℝ ↔
𝐴 ∈
ℝ)) |
87 | 83, 86 | syl5ib 234 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-𝐴 ∈
ℝ+ → 𝐴 ∈ ℝ)) |
88 | | lognegb 24336 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
89 | 8, 88 | syldan 487 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(-𝐴 ∈
ℝ+ ↔ (ℑ‘(log‘𝐴)) = π)) |
90 | | reim0b 13859 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
91 | 90 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
92 | 87, 89, 91 | 3imtr3d 282 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) = π → (ℑ‘𝐴) = 0)) |
93 | 92 | necon3d 2815 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘𝐴) ≠ 0
→ (ℑ‘(log‘𝐴)) ≠ π)) |
94 | 3, 93 | mpd 15 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≠ π) |
95 | 94 | necomd 2849 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
π ≠ (ℑ‘(log‘𝐴))) |
96 | 48 | simprd 479 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≤ π) |
97 | 11, 55, 96 | leltned 10190 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
((ℑ‘(log‘𝐴)) < π ↔ π ≠
(ℑ‘(log‘𝐴)))) |
98 | 95, 97 | mpbird 247 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) < π) |
99 | | 0xr 10086 |
. . 3
⊢ 0 ∈
ℝ* |
100 | 42 | rexri 10097 |
. . 3
⊢ π
∈ ℝ* |
101 | | elioo2 12216 |
. . 3
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝐴)) ∈ (0(,)π) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ 0 <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π))) |
102 | 99, 100, 101 | mp2an 708 |
. 2
⊢
((ℑ‘(log‘𝐴)) ∈ (0(,)π) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ 0 <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π)) |
103 | 11, 81, 98, 102 | syl3anbrc 1246 |
1
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℑ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ (0(,)π)) |