Proof of Theorem argregt0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | recl 15149 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) | 
| 2 |  | gt0ne0 11728 | . . . . . 6
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ≠ 0) | 
| 3 | 1, 2 | sylan 580 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘𝐴) ≠
0) | 
| 4 |  | fveq2 6906 | . . . . . . 7
⊢ (𝐴 = 0 → (ℜ‘𝐴) =
(ℜ‘0)) | 
| 5 |  | re0 15191 | . . . . . . 7
⊢
(ℜ‘0) = 0 | 
| 6 | 4, 5 | eqtrdi 2793 | . . . . . 6
⊢ (𝐴 = 0 → (ℜ‘𝐴) = 0) | 
| 7 | 6 | necon3i 2973 | . . . . 5
⊢
((ℜ‘𝐴)
≠ 0 → 𝐴 ≠
0) | 
| 8 | 3, 7 | syl 17 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
𝐴 ≠ 0) | 
| 9 |  | logcl 26610 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) | 
| 10 | 8, 9 | syldan 591 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(log‘𝐴) ∈
ℂ) | 
| 11 | 10 | imcld 15234 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℝ) | 
| 12 |  | coshalfpi 26511 | . . . . . 6
⊢
(cos‘(π / 2)) = 0 | 
| 13 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → 0
< (ℜ‘𝐴)) | 
| 14 |  | abscl 15317 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) | 
| 15 | 14 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘𝐴) ∈
ℝ) | 
| 16 | 15 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘𝐴) ∈
ℂ) | 
| 17 | 16 | mul01d 11460 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘𝐴) · 0)
= 0) | 
| 18 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
𝐴 ∈
ℂ) | 
| 19 |  | absrpcl 15327 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) | 
| 20 | 8, 19 | syldan 591 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘𝐴) ∈
ℝ+) | 
| 21 | 20 | rpne0d 13082 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘𝐴) ≠
0) | 
| 22 | 18, 16, 21 | divcld 12043 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(𝐴 / (abs‘𝐴)) ∈
ℂ) | 
| 23 | 15, 22 | remul2d 15266 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = ((abs‘𝐴) · (ℜ‘(𝐴 / (abs‘𝐴))))) | 
| 24 | 18, 16, 21 | divcan2d 12045 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘𝐴) ·
(𝐴 / (abs‘𝐴))) = 𝐴) | 
| 25 | 24 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = (ℜ‘𝐴)) | 
| 26 | 23, 25 | eqtr3d 2779 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘𝐴) ·
(ℜ‘(𝐴 /
(abs‘𝐴)))) =
(ℜ‘𝐴)) | 
| 27 | 13, 17, 26 | 3brtr4d 5175 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘𝐴) · 0)
< ((abs‘𝐴)
· (ℜ‘(𝐴 /
(abs‘𝐴))))) | 
| 28 |  | 0re 11263 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ | 
| 29 | 28 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → 0
∈ ℝ) | 
| 30 | 22 | recld 15233 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 /
(abs‘𝐴))) ∈
ℝ) | 
| 31 | 29, 30, 20 | ltmul2d 13119 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → (0
< (ℜ‘(𝐴 /
(abs‘𝐴))) ↔
((abs‘𝐴) · 0)
< ((abs‘𝐴)
· (ℜ‘(𝐴 /
(abs‘𝐴)))))) | 
| 32 | 27, 31 | mpbird 257 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → 0
< (ℜ‘(𝐴 /
(abs‘𝐴)))) | 
| 33 |  | efiarg 26649 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i
· (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) | 
| 34 | 8, 33 | syldan 591 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) | 
| 35 | 34 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(exp‘(i · (ℑ‘(log‘𝐴))))) = (ℜ‘(𝐴 / (abs‘𝐴)))) | 
| 36 | 32, 35 | breqtrrd 5171 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → 0
< (ℜ‘(exp‘(i · (ℑ‘(log‘𝐴)))))) | 
| 37 |  | recosval 16172 | . . . . . . . . 9
⊢
((ℑ‘(log‘𝐴)) ∈ ℝ →
(cos‘(ℑ‘(log‘𝐴))) = (ℜ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) | 
| 38 | 11, 37 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(cos‘(ℑ‘(log‘𝐴))) = (ℜ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) | 
| 39 | 36, 38 | breqtrrd 5171 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → 0
< (cos‘(ℑ‘(log‘𝐴)))) | 
| 40 |  | fveq2 6906 | . . . . . . . . 9
⊢
((abs‘(ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴)))) | 
| 41 | 40 | a1i 11 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴))))) | 
| 42 | 11 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℂ) | 
| 43 |  | cosneg 16183 | . . . . . . . . . 10
⊢
((ℑ‘(log‘𝐴)) ∈ ℂ →
(cos‘-(ℑ‘(log‘𝐴))) =
(cos‘(ℑ‘(log‘𝐴)))) | 
| 44 | 42, 43 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(cos‘-(ℑ‘(log‘𝐴))) =
(cos‘(ℑ‘(log‘𝐴)))) | 
| 45 |  | fveqeq2 6915 | . . . . . . . . 9
⊢
((abs‘(ℑ‘(log‘𝐴))) = -(ℑ‘(log‘𝐴)) →
((cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴))) ↔
(cos‘-(ℑ‘(log‘𝐴))) =
(cos‘(ℑ‘(log‘𝐴))))) | 
| 46 | 44, 45 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) = -(ℑ‘(log‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴))))) | 
| 47 | 11 | absord 15454 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐴)) ∨
(abs‘(ℑ‘(log‘𝐴))) = -(ℑ‘(log‘𝐴)))) | 
| 48 | 41, 46, 47 | mpjaod 861 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴)))) | 
| 49 | 39, 48 | breqtrrd 5171 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → 0
< (cos‘(abs‘(ℑ‘(log‘𝐴))))) | 
| 50 | 12, 49 | eqbrtrid 5178 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(cos‘(π / 2)) <
(cos‘(abs‘(ℑ‘(log‘𝐴))))) | 
| 51 | 42 | abscld 15475 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) ∈ ℝ) | 
| 52 | 42 | absge0d 15483 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) → 0
≤ (abs‘(ℑ‘(log‘𝐴)))) | 
| 53 |  | logimcl 26611 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) | 
| 54 | 8, 53 | syldan 591 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) | 
| 55 | 54 | simpld 494 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
-π < (ℑ‘(log‘𝐴))) | 
| 56 |  | pire 26500 | . . . . . . . . . . 11
⊢ π
∈ ℝ | 
| 57 | 56 | renegcli 11570 | . . . . . . . . . 10
⊢ -π
∈ ℝ | 
| 58 |  | ltle 11349 | . . . . . . . . . 10
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) | 
| 59 | 57, 11, 58 | sylancr 587 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) | 
| 60 | 55, 59 | mpd 15 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
-π ≤ (ℑ‘(log‘𝐴))) | 
| 61 | 54 | simprd 495 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≤ π) | 
| 62 |  | absle 15354 | . . . . . . . . 9
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ)
→ ((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) | 
| 63 | 11, 56, 62 | sylancl 586 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) | 
| 64 | 60, 61, 63 | mpbir2and 713 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) ≤ π) | 
| 65 | 28, 56 | elicc2i 13453 | . . . . . . 7
⊢
((abs‘(ℑ‘(log‘𝐴))) ∈ (0[,]π) ↔
((abs‘(ℑ‘(log‘𝐴))) ∈ ℝ ∧ 0 ≤
(abs‘(ℑ‘(log‘𝐴))) ∧
(abs‘(ℑ‘(log‘𝐴))) ≤ π)) | 
| 66 | 51, 52, 64, 65 | syl3anbrc 1344 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) ∈ (0[,]π)) | 
| 67 |  | halfpire 26506 | . . . . . . 7
⊢ (π /
2) ∈ ℝ | 
| 68 |  | pirp 26503 | . . . . . . . 8
⊢ π
∈ ℝ+ | 
| 69 |  | rphalfcl 13062 | . . . . . . . 8
⊢ (π
∈ ℝ+ → (π / 2) ∈
ℝ+) | 
| 70 |  | rpge0 13048 | . . . . . . . 8
⊢ ((π /
2) ∈ ℝ+ → 0 ≤ (π / 2)) | 
| 71 | 68, 69, 70 | mp2b 10 | . . . . . . 7
⊢ 0 ≤
(π / 2) | 
| 72 |  | rphalflt 13064 | . . . . . . . . 9
⊢ (π
∈ ℝ+ → (π / 2) < π) | 
| 73 | 68, 72 | ax-mp 5 | . . . . . . . 8
⊢ (π /
2) < π | 
| 74 | 67, 56, 73 | ltleii 11384 | . . . . . . 7
⊢ (π /
2) ≤ π | 
| 75 | 28, 56 | elicc2i 13453 | . . . . . . 7
⊢ ((π /
2) ∈ (0[,]π) ↔ ((π / 2) ∈ ℝ ∧ 0 ≤ (π / 2)
∧ (π / 2) ≤ π)) | 
| 76 | 67, 71, 74, 75 | mpbir3an 1342 | . . . . . 6
⊢ (π /
2) ∈ (0[,]π) | 
| 77 |  | cosord 26573 | . . . . . 6
⊢
(((abs‘(ℑ‘(log‘𝐴))) ∈ (0[,]π) ∧ (π / 2)
∈ (0[,]π)) → ((abs‘(ℑ‘(log‘𝐴))) < (π / 2) ↔
(cos‘(π / 2)) <
(cos‘(abs‘(ℑ‘(log‘𝐴)))))) | 
| 78 | 66, 76, 77 | sylancl 586 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) < (π / 2) ↔ (cos‘(π
/ 2)) < (cos‘(abs‘(ℑ‘(log‘𝐴)))))) | 
| 79 | 50, 78 | mpbird 257 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) < (π / 2)) | 
| 80 |  | abslt 15353 | . . . . 5
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ (π / 2) ∈
ℝ) → ((abs‘(ℑ‘(log‘𝐴))) < (π / 2) ↔ (-(π / 2) <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < (π /
2)))) | 
| 81 | 11, 67, 80 | sylancl 586 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) < (π / 2) ↔ (-(π / 2) <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < (π /
2)))) | 
| 82 | 79, 81 | mpbid 232 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(-(π / 2) < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < (π /
2))) | 
| 83 | 82 | simpld 494 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
-(π / 2) < (ℑ‘(log‘𝐴))) | 
| 84 | 82 | simprd 495 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) < (π / 2)) | 
| 85 | 67 | renegcli 11570 | . . . 4
⊢ -(π /
2) ∈ ℝ | 
| 86 | 85 | rexri 11319 | . . 3
⊢ -(π /
2) ∈ ℝ* | 
| 87 | 67 | rexri 11319 | . . 3
⊢ (π /
2) ∈ ℝ* | 
| 88 |  | elioo2 13428 | . . 3
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*)
→ ((ℑ‘(log‘𝐴)) ∈ (-(π / 2)(,)(π / 2)) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ -(π / 2) <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < (π /
2)))) | 
| 89 | 86, 87, 88 | mp2an 692 | . 2
⊢
((ℑ‘(log‘𝐴)) ∈ (-(π / 2)(,)(π / 2)) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ -(π / 2) <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < (π /
2))) | 
| 90 | 11, 83, 84, 89 | syl3anbrc 1344 | 1
⊢ ((𝐴 ∈ ℂ ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ (-(π / 2)(,)(π /
2))) |