Proof of Theorem absefib
Step | Hyp | Ref
| Expression |
1 | | ef0 15443 |
. . . . 5
⊢
(exp‘0) = 1 |
2 | 1 | eqeq2i 2834 |
. . . 4
⊢
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
(exp‘-(ℑ‘𝐴)) = 1) |
3 | | imcl 14469 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
4 | 3 | renegcld 11066 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) |
5 | | 0re 10642 |
. . . . 5
⊢ 0 ∈
ℝ |
6 | | reef11 15471 |
. . . . 5
⊢
((-(ℑ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) |
7 | 4, 5, 6 | sylancl 588 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) |
8 | 2, 7 | syl5bbr 287 |
. . 3
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = 1 ↔ -(ℑ‘𝐴) = 0)) |
9 | 3 | recnd 10668 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) |
10 | 9 | negeq0d 10988 |
. . 3
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) = 0
↔ -(ℑ‘𝐴) =
0)) |
11 | 8, 10 | bitr4d 284 |
. 2
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = 1 ↔ (ℑ‘𝐴) = 0)) |
12 | | ax-icn 10595 |
. . . . . 6
⊢ i ∈
ℂ |
13 | | mulcl 10620 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
14 | 12, 13 | mpan 688 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) |
15 | | absef 15549 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (abs‘(exp‘(i · 𝐴))) = (exp‘(ℜ‘(i ·
𝐴)))) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · 𝐴))) = (exp‘(ℜ‘(i ·
𝐴)))) |
17 | | recl 14468 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
18 | 17 | recnd 10668 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) |
19 | | mulcl 10620 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
20 | 12, 9, 19 | sylancr 589 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (ℑ‘𝐴))
∈ ℂ) |
21 | | replim 14474 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
22 | 18, 20, 21 | comraddd 10853 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 𝐴 = ((i ·
(ℑ‘𝐴)) +
(ℜ‘𝐴))) |
23 | 22 | oveq2d 7171 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) = (i ·
((i · (ℑ‘𝐴)) + (ℜ‘𝐴)))) |
24 | | adddi 10625 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (i · (ℑ‘𝐴)) ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = ((i · (i ·
(ℑ‘𝐴))) + (i
· (ℜ‘𝐴)))) |
25 | 12, 20, 18, 24 | mp3an2i 1462 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = ((i · (i ·
(ℑ‘𝐴))) + (i
· (ℜ‘𝐴)))) |
26 | | ixi 11268 |
. . . . . . . . . . . 12
⊢ (i
· i) = -1 |
27 | 26 | oveq1i 7165 |
. . . . . . . . . . 11
⊢ ((i
· i) · (ℑ‘𝐴)) = (-1 · (ℑ‘𝐴)) |
28 | | mulass 10624 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → ((i · i)
· (ℑ‘𝐴))
= (i · (i · (ℑ‘𝐴)))) |
29 | 12, 12, 9, 28 | mp3an12i 1461 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((i
· i) · (ℑ‘𝐴)) = (i · (i ·
(ℑ‘𝐴)))) |
30 | 9 | mulm1d 11091 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) |
31 | 27, 29, 30 | 3eqtr3a 2880 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (i · (ℑ‘𝐴))) = -(ℑ‘𝐴)) |
32 | 31 | oveq1d 7170 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((i
· (i · (ℑ‘𝐴))) + (i · (ℜ‘𝐴))) = (-(ℑ‘𝐴) + (i ·
(ℜ‘𝐴)))) |
33 | 25, 32 | eqtrd 2856 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = (-(ℑ‘𝐴) + (i · (ℜ‘𝐴)))) |
34 | 23, 33 | eqtrd 2856 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) =
(-(ℑ‘𝐴) + (i
· (ℜ‘𝐴)))) |
35 | 34 | fveq2d 6673 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘(i · 𝐴)) = (ℜ‘(-(ℑ‘𝐴) + (i ·
(ℜ‘𝐴))))) |
36 | 4, 17 | crred 14589 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘(-(ℑ‘𝐴) + (i · (ℜ‘𝐴)))) = -(ℑ‘𝐴)) |
37 | 35, 36 | eqtrd 2856 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(ℜ‘(i · 𝐴)) = -(ℑ‘𝐴)) |
38 | 37 | fveq2d 6673 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(exp‘(ℜ‘(i · 𝐴))) = (exp‘-(ℑ‘𝐴))) |
39 | 16, 38 | eqtrd 2856 |
. . 3
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · 𝐴))) = (exp‘-(ℑ‘𝐴))) |
40 | 39 | eqeq1d 2823 |
. 2
⊢ (𝐴 ∈ ℂ →
((abs‘(exp‘(i · 𝐴))) = 1 ↔
(exp‘-(ℑ‘𝐴)) = 1)) |
41 | | reim0b 14477 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
42 | 11, 40, 41 | 3bitr4rd 314 |
1
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(abs‘(exp‘(i · 𝐴))) = 1)) |