Proof of Theorem efieq1re
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | replim 15156 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) | 
| 2 | 1 | oveq2d 7448 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) = (i ·
((ℜ‘𝐴) + (i
· (ℑ‘𝐴))))) | 
| 3 |  | ax-icn 11215 | . . . . . . . . . 10
⊢ i ∈
ℂ | 
| 4 |  | recl 15150 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) | 
| 5 | 4 | recnd 11290 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) | 
| 6 |  | imcl 15151 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) | 
| 7 | 6 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) | 
| 8 |  | mulcl 11240 | . . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) | 
| 9 | 3, 7, 8 | sylancr 587 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (ℑ‘𝐴))
∈ ℂ) | 
| 10 |  | adddi 11245 | . . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ ∧ (i ·
(ℑ‘𝐴)) ∈
ℂ) → (i · ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) = ((i ·
(ℜ‘𝐴)) + (i
· (i · (ℑ‘𝐴))))) | 
| 11 | 3, 5, 9, 10 | mp3an2i 1467 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (i
· ((ℜ‘𝐴)
+ (i · (ℑ‘𝐴)))) = ((i · (ℜ‘𝐴)) + (i · (i ·
(ℑ‘𝐴))))) | 
| 12 |  | ixi 11893 | . . . . . . . . . . . 12
⊢ (i
· i) = -1 | 
| 13 | 12 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((i
· i) · (ℑ‘𝐴)) = (-1 · (ℑ‘𝐴)) | 
| 14 |  | mulass 11244 | . . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → ((i · i)
· (ℑ‘𝐴))
= (i · (i · (ℑ‘𝐴)))) | 
| 15 | 3, 3, 7, 14 | mp3an12i 1466 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((i
· i) · (ℑ‘𝐴)) = (i · (i ·
(ℑ‘𝐴)))) | 
| 16 | 7 | mulm1d 11716 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) | 
| 17 | 13, 15, 16 | 3eqtr3a 2800 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (i · (ℑ‘𝐴))) = -(ℑ‘𝐴)) | 
| 18 | 17 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((i
· (ℜ‘𝐴))
+ (i · (i · (ℑ‘𝐴)))) = ((i · (ℜ‘𝐴)) + -(ℑ‘𝐴))) | 
| 19 | 11, 18 | eqtrd 2776 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· ((ℜ‘𝐴)
+ (i · (ℑ‘𝐴)))) = ((i · (ℜ‘𝐴)) + -(ℑ‘𝐴))) | 
| 20 | 2, 19 | eqtrd 2776 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) = ((i ·
(ℜ‘𝐴)) +
-(ℑ‘𝐴))) | 
| 21 | 20 | fveq2d 6909 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= (exp‘((i · (ℜ‘𝐴)) + -(ℑ‘𝐴)))) | 
| 22 |  | mulcl 11240 | . . . . . . . 8
⊢ ((i
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (i ·
(ℜ‘𝐴)) ∈
ℂ) | 
| 23 | 3, 5, 22 | sylancr 587 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· (ℜ‘𝐴))
∈ ℂ) | 
| 24 | 6 | renegcld 11691 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) | 
| 25 | 24 | recnd 11290 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℂ) | 
| 26 |  | efadd 16131 | . . . . . . 7
⊢ (((i
· (ℜ‘𝐴))
∈ ℂ ∧ -(ℑ‘𝐴) ∈ ℂ) → (exp‘((i
· (ℜ‘𝐴))
+ -(ℑ‘𝐴))) =
((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) | 
| 27 | 23, 25, 26 | syl2anc 584 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘((i · (ℜ‘𝐴)) + -(ℑ‘𝐴))) = ((exp‘(i ·
(ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) | 
| 28 | 21, 27 | eqtrd 2776 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) | 
| 29 | 28 | eqeq1d 2738 | . . . 4
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
= 1 ↔ ((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1)) | 
| 30 |  | efcl 16119 | . . . . . . . . 9
⊢ ((i
· (ℜ‘𝐴))
∈ ℂ → (exp‘(i · (ℜ‘𝐴))) ∈ ℂ) | 
| 31 | 23, 30 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘(i · (ℜ‘𝐴))) ∈ ℂ) | 
| 32 |  | efcl 16119 | . . . . . . . . 9
⊢
(-(ℑ‘𝐴)
∈ ℂ → (exp‘-(ℑ‘𝐴)) ∈ ℂ) | 
| 33 | 25, 32 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘-(ℑ‘𝐴)) ∈ ℂ) | 
| 34 | 31, 33 | absmuld 15494 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(abs‘((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) = ((abs‘(exp‘(i ·
(ℜ‘𝐴))))
· (abs‘(exp‘-(ℑ‘𝐴))))) | 
| 35 |  | absefi 16233 | . . . . . . . . 9
⊢
((ℜ‘𝐴)
∈ ℝ → (abs‘(exp‘(i · (ℜ‘𝐴)))) = 1) | 
| 36 | 4, 35 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · (ℜ‘𝐴)))) = 1) | 
| 37 | 24 | reefcld 16125 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘-(ℑ‘𝐴)) ∈ ℝ) | 
| 38 |  | efgt0 16140 | . . . . . . . . . . 11
⊢
(-(ℑ‘𝐴)
∈ ℝ → 0 < (exp‘-(ℑ‘𝐴))) | 
| 39 | 24, 38 | syl 17 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 0 <
(exp‘-(ℑ‘𝐴))) | 
| 40 |  | 0re 11264 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ | 
| 41 |  | ltle 11350 | . . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (exp‘-(ℑ‘𝐴)) ∈ ℝ) → (0 <
(exp‘-(ℑ‘𝐴)) → 0 ≤
(exp‘-(ℑ‘𝐴)))) | 
| 42 | 40, 41 | mpan 690 | . . . . . . . . . 10
⊢
((exp‘-(ℑ‘𝐴)) ∈ ℝ → (0 <
(exp‘-(ℑ‘𝐴)) → 0 ≤
(exp‘-(ℑ‘𝐴)))) | 
| 43 | 37, 39, 42 | sylc 65 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 0 ≤
(exp‘-(ℑ‘𝐴))) | 
| 44 | 37, 43 | absidd 15462 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘-(ℑ‘𝐴))) = (exp‘-(ℑ‘𝐴))) | 
| 45 | 36, 44 | oveq12d 7450 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
((abs‘(exp‘(i · (ℜ‘𝐴)))) ·
(abs‘(exp‘-(ℑ‘𝐴)))) = (1 ·
(exp‘-(ℑ‘𝐴)))) | 
| 46 | 33 | mullidd 11280 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (1
· (exp‘-(ℑ‘𝐴))) = (exp‘-(ℑ‘𝐴))) | 
| 47 | 34, 45, 46 | 3eqtrrd 2781 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘-(ℑ‘𝐴)) = (abs‘((exp‘(i ·
(ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))))) | 
| 48 |  | fveq2 6905 | . . . . . 6
⊢
(((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1 → (abs‘((exp‘(i
· (ℜ‘𝐴)))
· (exp‘-(ℑ‘𝐴)))) = (abs‘1)) | 
| 49 | 47, 48 | sylan9eq 2796 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1) →
(exp‘-(ℑ‘𝐴)) = (abs‘1)) | 
| 50 | 49 | ex 412 | . . . 4
⊢ (𝐴 ∈ ℂ →
(((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1 →
(exp‘-(ℑ‘𝐴)) = (abs‘1))) | 
| 51 | 29, 50 | sylbid 240 | . . 3
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
= 1 → (exp‘-(ℑ‘𝐴)) = (abs‘1))) | 
| 52 | 7 | negeq0d 11613 | . . . 4
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) = 0
↔ -(ℑ‘𝐴) =
0)) | 
| 53 |  | reim0b 15159 | . . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) | 
| 54 |  | ef0 16128 | . . . . . . 7
⊢
(exp‘0) = 1 | 
| 55 |  | abs1 15337 | . . . . . . 7
⊢
(abs‘1) = 1 | 
| 56 | 54, 55 | eqtr4i 2767 | . . . . . 6
⊢
(exp‘0) = (abs‘1) | 
| 57 | 56 | eqeq2i 2749 | . . . . 5
⊢
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
(exp‘-(ℑ‘𝐴)) = (abs‘1)) | 
| 58 |  | reef11 16156 | . . . . . 6
⊢
((-(ℑ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) | 
| 59 | 24, 40, 58 | sylancl 586 | . . . . 5
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) | 
| 60 | 57, 59 | bitr3id 285 | . . . 4
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (abs‘1) ↔
-(ℑ‘𝐴) =
0)) | 
| 61 | 52, 53, 60 | 3bitr4rd 312 | . . 3
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (abs‘1) ↔ 𝐴 ∈ ℝ)) | 
| 62 | 51, 61 | sylibd 239 | . 2
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
= 1 → 𝐴 ∈
ℝ)) | 
| 63 | 62 | imp 406 | 1
⊢ ((𝐴 ∈ ℂ ∧
(exp‘(i · 𝐴))
= 1) → 𝐴 ∈
ℝ) |