Proof of Theorem absefib
Step | Hyp | Ref
| Expression |
1 | | ef0 11628 |
. . . . 5
⊢
(exp‘0) = 1 |
2 | 1 | eqeq2i 2181 |
. . . 4
⊢
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
(exp‘-(ℑ‘𝐴)) = 1) |
3 | | imcl 10811 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
4 | 3 | renegcld 8292 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) |
5 | | 0re 7913 |
. . . . 5
⊢ 0 ∈
ℝ |
6 | | reef11 11655 |
. . . . 5
⊢
((-(ℑ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) |
7 | 4, 5, 6 | sylancl 411 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) |
8 | 2, 7 | bitr3id 193 |
. . 3
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = 1 ↔ -(ℑ‘𝐴) = 0)) |
9 | 3 | recnd 7941 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) |
10 | 9 | negeq0d 8215 |
. . 3
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) = 0
↔ -(ℑ‘𝐴) =
0)) |
11 | 8, 10 | bitr4d 190 |
. 2
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = 1 ↔ (ℑ‘𝐴) = 0)) |
12 | | ax-icn 7862 |
. . . . . 6
⊢ i ∈
ℂ |
13 | | mulcl 7894 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
14 | 12, 13 | mpan 422 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) |
15 | | absef 11725 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (abs‘(exp‘(i · 𝐴))) = (exp‘(ℜ‘(i ·
𝐴)))) |
16 | 14, 15 | syl 14 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · 𝐴))) = (exp‘(ℜ‘(i ·
𝐴)))) |
17 | | replim 10816 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
18 | | recl 10810 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
19 | 18 | recnd 7941 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) |
20 | | mulcl 7894 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
21 | 12, 9, 20 | sylancr 412 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (i
· (ℑ‘𝐴))
∈ ℂ) |
22 | 19, 21 | addcomd 8063 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) = ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) |
23 | 17, 22 | eqtrd 2203 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 𝐴 = ((i ·
(ℑ‘𝐴)) +
(ℜ‘𝐴))) |
24 | 23 | oveq2d 5867 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) = (i ·
((i · (ℑ‘𝐴)) + (ℜ‘𝐴)))) |
25 | | adddi 7899 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (i · (ℑ‘𝐴)) ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = ((i · (i ·
(ℑ‘𝐴))) + (i
· (ℜ‘𝐴)))) |
26 | 12, 25 | mp3an1 1319 |
. . . . . . . . . 10
⊢ (((i
· (ℑ‘𝐴))
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (i · ((i
· (ℑ‘𝐴))
+ (ℜ‘𝐴))) = ((i
· (i · (ℑ‘𝐴))) + (i · (ℜ‘𝐴)))) |
27 | 21, 19, 26 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = ((i · (i ·
(ℑ‘𝐴))) + (i
· (ℜ‘𝐴)))) |
28 | | ixi 8495 |
. . . . . . . . . . . 12
⊢ (i
· i) = -1 |
29 | 28 | oveq1i 5861 |
. . . . . . . . . . 11
⊢ ((i
· i) · (ℑ‘𝐴)) = (-1 · (ℑ‘𝐴)) |
30 | | mulass 7898 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → ((i · i)
· (ℑ‘𝐴))
= (i · (i · (ℑ‘𝐴)))) |
31 | 12, 12, 30 | mp3an12 1322 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝐴)
∈ ℂ → ((i · i) · (ℑ‘𝐴)) = (i · (i ·
(ℑ‘𝐴)))) |
32 | 9, 31 | syl 14 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((i
· i) · (ℑ‘𝐴)) = (i · (i ·
(ℑ‘𝐴)))) |
33 | 9 | mulm1d 8322 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) |
34 | 29, 32, 33 | 3eqtr3a 2227 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (i · (ℑ‘𝐴))) = -(ℑ‘𝐴)) |
35 | 34 | oveq1d 5866 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((i
· (i · (ℑ‘𝐴))) + (i · (ℜ‘𝐴))) = (-(ℑ‘𝐴) + (i ·
(ℜ‘𝐴)))) |
36 | 27, 35 | eqtrd 2203 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = (-(ℑ‘𝐴) + (i · (ℜ‘𝐴)))) |
37 | 24, 36 | eqtrd 2203 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) =
(-(ℑ‘𝐴) + (i
· (ℜ‘𝐴)))) |
38 | 37 | fveq2d 5498 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘(i · 𝐴)) = (ℜ‘(-(ℑ‘𝐴) + (i ·
(ℜ‘𝐴))))) |
39 | 4, 18 | crred 10933 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘(-(ℑ‘𝐴) + (i · (ℜ‘𝐴)))) = -(ℑ‘𝐴)) |
40 | 38, 39 | eqtrd 2203 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(ℜ‘(i · 𝐴)) = -(ℑ‘𝐴)) |
41 | 40 | fveq2d 5498 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(exp‘(ℜ‘(i · 𝐴))) = (exp‘-(ℑ‘𝐴))) |
42 | 16, 41 | eqtrd 2203 |
. . 3
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · 𝐴))) = (exp‘-(ℑ‘𝐴))) |
43 | 42 | eqeq1d 2179 |
. 2
⊢ (𝐴 ∈ ℂ →
((abs‘(exp‘(i · 𝐴))) = 1 ↔
(exp‘-(ℑ‘𝐴)) = 1)) |
44 | | reim0b 10819 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
45 | 11, 43, 44 | 3bitr4rd 220 |
1
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(abs‘(exp‘(i · 𝐴))) = 1)) |