Proof of Theorem logcj
Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . 7
⊢ (𝐴 = 0 → (ℑ‘𝐴) =
(ℑ‘0)) |
2 | | im0 13741 |
. . . . . . 7
⊢
(ℑ‘0) = 0 |
3 | 1, 2 | syl6eq 2660 |
. . . . . 6
⊢ (𝐴 = 0 → (ℑ‘𝐴) = 0) |
4 | 3 | necon3i 2814 |
. . . . 5
⊢
((ℑ‘𝐴)
≠ 0 → 𝐴 ≠
0) |
5 | | logcl 24119 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
6 | 4, 5 | sylan2 490 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (log‘𝐴) ∈
ℂ) |
7 | | efcj 14661 |
. . . 4
⊢
((log‘𝐴)
∈ ℂ → (exp‘(∗‘(log‘𝐴))) =
(∗‘(exp‘(log‘𝐴)))) |
8 | 6, 7 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (exp‘(∗‘(log‘𝐴))) =
(∗‘(exp‘(log‘𝐴)))) |
9 | | eflog 24127 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
10 | 4, 9 | sylan2 490 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (exp‘(log‘𝐴)) = 𝐴) |
11 | 10 | fveq2d 6107 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (∗‘(exp‘(log‘𝐴))) = (∗‘𝐴)) |
12 | 8, 11 | eqtrd 2644 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (exp‘(∗‘(log‘𝐴))) = (∗‘𝐴)) |
13 | | cjcl 13693 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) ∈
ℂ) |
14 | 13 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (∗‘𝐴)
∈ ℂ) |
15 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (ℑ‘𝐴)
≠ 0) |
16 | 15, 4 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ 𝐴 ≠
0) |
17 | | cjne0 13751 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔
(∗‘𝐴) ≠
0)) |
18 | 17 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (𝐴 ≠ 0 ↔
(∗‘𝐴) ≠
0)) |
19 | 16, 18 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (∗‘𝐴)
≠ 0) |
20 | 6 | cjcld 13784 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (∗‘(log‘𝐴)) ∈ ℂ) |
21 | | rpre 11715 |
. . . . . . . . . . . . 13
⊢ (-𝐴 ∈ ℝ+
→ -𝐴 ∈
ℝ) |
22 | 21 | renegcld 10336 |
. . . . . . . . . . . 12
⊢ (-𝐴 ∈ ℝ+
→ --𝐴 ∈
ℝ) |
23 | | negneg 10210 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ --𝐴 = 𝐴) |
25 | 24 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (--𝐴 ∈ ℝ
↔ 𝐴 ∈
ℝ)) |
26 | 22, 25 | syl5ib 233 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (-𝐴 ∈
ℝ+ → 𝐴 ∈ ℝ)) |
27 | | lognegb 24140 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
28 | 4, 27 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (-𝐴 ∈
ℝ+ ↔ (ℑ‘(log‘𝐴)) = π)) |
29 | | reim0b 13707 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (𝐴 ∈ ℝ
↔ (ℑ‘𝐴) =
0)) |
31 | 26, 28, 30 | 3imtr3d 281 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ ((ℑ‘(log‘𝐴)) = π → (ℑ‘𝐴) = 0)) |
32 | 31 | necon3d 2803 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ ((ℑ‘𝐴)
≠ 0 → (ℑ‘(log‘𝐴)) ≠ π)) |
33 | 15, 32 | mpd 15 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (ℑ‘(log‘𝐴)) ≠ π) |
34 | 33 | necomd 2837 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ π ≠ (ℑ‘(log‘𝐴))) |
35 | 6 | imcld 13783 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (ℑ‘(log‘𝐴)) ∈ ℝ) |
36 | | pire 24014 |
. . . . . . . . 9
⊢ π
∈ ℝ |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ π ∈ ℝ) |
38 | | logimcl 24120 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
39 | 4, 38 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
40 | 39 | simprd 478 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (ℑ‘(log‘𝐴)) ≤ π) |
41 | 35, 37, 40 | leltned 10069 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ ((ℑ‘(log‘𝐴)) < π ↔ π ≠
(ℑ‘(log‘𝐴)))) |
42 | 34, 41 | mpbird 246 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (ℑ‘(log‘𝐴)) < π) |
43 | | ltneg 10407 |
. . . . . . 7
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ)
→ ((ℑ‘(log‘𝐴)) < π ↔ -π <
-(ℑ‘(log‘𝐴)))) |
44 | 35, 36, 43 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ ((ℑ‘(log‘𝐴)) < π ↔ -π <
-(ℑ‘(log‘𝐴)))) |
45 | 42, 44 | mpbid 221 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ -π < -(ℑ‘(log‘𝐴))) |
46 | 6 | imcjd 13793 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (ℑ‘(∗‘(log‘𝐴))) = -(ℑ‘(log‘𝐴))) |
47 | 45, 46 | breqtrrd 4611 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ -π < (ℑ‘(∗‘(log‘𝐴)))) |
48 | 39 | simpld 474 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ -π < (ℑ‘(log‘𝐴))) |
49 | 36 | renegcli 10221 |
. . . . . . . 8
⊢ -π
∈ ℝ |
50 | | ltle 10005 |
. . . . . . . 8
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
51 | 49, 35, 50 | sylancr 694 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (-π < (ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
52 | 48, 51 | mpd 15 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ -π ≤ (ℑ‘(log‘𝐴))) |
53 | | lenegcon1 10411 |
. . . . . . 7
⊢ ((π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π ≤
(ℑ‘(log‘𝐴)) ↔ -(ℑ‘(log‘𝐴)) ≤ π)) |
54 | 36, 35, 53 | sylancr 694 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (-π ≤ (ℑ‘(log‘𝐴)) ↔ -(ℑ‘(log‘𝐴)) ≤ π)) |
55 | 52, 54 | mpbid 221 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ -(ℑ‘(log‘𝐴)) ≤ π) |
56 | 46, 55 | eqbrtrd 4605 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (ℑ‘(∗‘(log‘𝐴))) ≤ π) |
57 | | ellogrn 24110 |
. . . 4
⊢
((∗‘(log‘𝐴)) ∈ ran log ↔
((∗‘(log‘𝐴)) ∈ ℂ ∧ -π <
(ℑ‘(∗‘(log‘𝐴))) ∧
(ℑ‘(∗‘(log‘𝐴))) ≤ π)) |
58 | 20, 47, 56, 57 | syl3anbrc 1239 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (∗‘(log‘𝐴)) ∈ ran log) |
59 | | logeftb 24134 |
. . 3
⊢
(((∗‘𝐴)
∈ ℂ ∧ (∗‘𝐴) ≠ 0 ∧
(∗‘(log‘𝐴)) ∈ ran log) →
((log‘(∗‘𝐴)) = (∗‘(log‘𝐴)) ↔
(exp‘(∗‘(log‘𝐴))) = (∗‘𝐴))) |
60 | 14, 19, 58, 59 | syl3anc 1318 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ ((log‘(∗‘𝐴)) = (∗‘(log‘𝐴)) ↔
(exp‘(∗‘(log‘𝐴))) = (∗‘𝐴))) |
61 | 12, 60 | mpbird 246 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≠ 0)
→ (log‘(∗‘𝐴)) = (∗‘(log‘𝐴))) |