Proof of Theorem absefib
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ef0 16128 | . . . . 5
⊢
(exp‘0) = 1 | 
| 2 | 1 | eqeq2i 2749 | . . . 4
⊢
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
(exp‘-(ℑ‘𝐴)) = 1) | 
| 3 |  | imcl 15151 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) | 
| 4 | 3 | renegcld 11691 | . . . . 5
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) | 
| 5 |  | 0re 11264 | . . . . 5
⊢ 0 ∈
ℝ | 
| 6 |  | reef11 16156 | . . . . 5
⊢
((-(ℑ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . 4
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) | 
| 8 | 2, 7 | bitr3id 285 | . . 3
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = 1 ↔ -(ℑ‘𝐴) = 0)) | 
| 9 | 3 | recnd 11290 | . . . 4
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) | 
| 10 | 9 | negeq0d 11613 | . . 3
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) = 0
↔ -(ℑ‘𝐴) =
0)) | 
| 11 | 8, 10 | bitr4d 282 | . 2
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = 1 ↔ (ℑ‘𝐴) = 0)) | 
| 12 |  | ax-icn 11215 | . . . . . 6
⊢ i ∈
ℂ | 
| 13 |  | mulcl 11240 | . . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 14 | 12, 13 | mpan 690 | . . . . 5
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) | 
| 15 |  | absef 16234 | . . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (abs‘(exp‘(i · 𝐴))) = (exp‘(ℜ‘(i ·
𝐴)))) | 
| 16 | 14, 15 | syl 17 | . . . 4
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · 𝐴))) = (exp‘(ℜ‘(i ·
𝐴)))) | 
| 17 |  | recl 15150 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) | 
| 18 | 17 | recnd 11290 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) | 
| 19 |  | mulcl 11240 | . . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) | 
| 20 | 12, 9, 19 | sylancr 587 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (ℑ‘𝐴))
∈ ℂ) | 
| 21 |  | replim 15156 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) | 
| 22 | 18, 20, 21 | comraddd 11476 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 𝐴 = ((i ·
(ℑ‘𝐴)) +
(ℜ‘𝐴))) | 
| 23 | 22 | oveq2d 7448 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) = (i ·
((i · (ℑ‘𝐴)) + (ℜ‘𝐴)))) | 
| 24 |  | adddi 11245 | . . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (i · (ℑ‘𝐴)) ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = ((i · (i ·
(ℑ‘𝐴))) + (i
· (ℜ‘𝐴)))) | 
| 25 | 12, 20, 18, 24 | mp3an2i 1467 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = ((i · (i ·
(ℑ‘𝐴))) + (i
· (ℜ‘𝐴)))) | 
| 26 |  | ixi 11893 | . . . . . . . . . . . 12
⊢ (i
· i) = -1 | 
| 27 | 26 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((i
· i) · (ℑ‘𝐴)) = (-1 · (ℑ‘𝐴)) | 
| 28 |  | mulass 11244 | . . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → ((i · i)
· (ℑ‘𝐴))
= (i · (i · (ℑ‘𝐴)))) | 
| 29 | 12, 12, 9, 28 | mp3an12i 1466 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((i
· i) · (ℑ‘𝐴)) = (i · (i ·
(ℑ‘𝐴)))) | 
| 30 | 9 | mulm1d 11716 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) | 
| 31 | 27, 29, 30 | 3eqtr3a 2800 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (i · (ℑ‘𝐴))) = -(ℑ‘𝐴)) | 
| 32 | 31 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((i
· (i · (ℑ‘𝐴))) + (i · (ℜ‘𝐴))) = (-(ℑ‘𝐴) + (i ·
(ℜ‘𝐴)))) | 
| 33 | 25, 32 | eqtrd 2776 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· ((i · (ℑ‘𝐴)) + (ℜ‘𝐴))) = (-(ℑ‘𝐴) + (i · (ℜ‘𝐴)))) | 
| 34 | 23, 33 | eqtrd 2776 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) =
(-(ℑ‘𝐴) + (i
· (ℜ‘𝐴)))) | 
| 35 | 34 | fveq2d 6909 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘(i · 𝐴)) = (ℜ‘(-(ℑ‘𝐴) + (i ·
(ℜ‘𝐴))))) | 
| 36 | 4, 17 | crred 15271 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘(-(ℑ‘𝐴) + (i · (ℜ‘𝐴)))) = -(ℑ‘𝐴)) | 
| 37 | 35, 36 | eqtrd 2776 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(ℜ‘(i · 𝐴)) = -(ℑ‘𝐴)) | 
| 38 | 37 | fveq2d 6909 | . . . 4
⊢ (𝐴 ∈ ℂ →
(exp‘(ℜ‘(i · 𝐴))) = (exp‘-(ℑ‘𝐴))) | 
| 39 | 16, 38 | eqtrd 2776 | . . 3
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · 𝐴))) = (exp‘-(ℑ‘𝐴))) | 
| 40 | 39 | eqeq1d 2738 | . 2
⊢ (𝐴 ∈ ℂ →
((abs‘(exp‘(i · 𝐴))) = 1 ↔
(exp‘-(ℑ‘𝐴)) = 1)) | 
| 41 |  | reim0b 15159 | . 2
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) | 
| 42 | 11, 40, 41 | 3bitr4rd 312 | 1
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(abs‘(exp‘(i · 𝐴))) = 1)) |