Proof of Theorem efieq1re
Step | Hyp | Ref
| Expression |
1 | | replim 10823 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
2 | 1 | oveq2d 5869 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) = (i ·
((ℜ‘𝐴) + (i
· (ℑ‘𝐴))))) |
3 | | recl 10817 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
4 | 3 | recnd 7948 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) |
5 | | ax-icn 7869 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
6 | | imcl 10818 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
7 | 6 | recnd 7948 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) |
8 | | mulcl 7901 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
9 | 5, 7, 8 | sylancr 412 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (ℑ‘𝐴))
∈ ℂ) |
10 | | adddi 7906 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ ∧ (i ·
(ℑ‘𝐴)) ∈
ℂ) → (i · ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) = ((i ·
(ℜ‘𝐴)) + (i
· (i · (ℑ‘𝐴))))) |
11 | 5, 10 | mp3an1 1319 |
. . . . . . . . . 10
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (i · (ℑ‘𝐴)) ∈ ℂ) → (i ·
((ℜ‘𝐴) + (i
· (ℑ‘𝐴)))) = ((i · (ℜ‘𝐴)) + (i · (i ·
(ℑ‘𝐴))))) |
12 | 4, 9, 11 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (i
· ((ℜ‘𝐴)
+ (i · (ℑ‘𝐴)))) = ((i · (ℜ‘𝐴)) + (i · (i ·
(ℑ‘𝐴))))) |
13 | | ixi 8502 |
. . . . . . . . . . . 12
⊢ (i
· i) = -1 |
14 | 13 | oveq1i 5863 |
. . . . . . . . . . 11
⊢ ((i
· i) · (ℑ‘𝐴)) = (-1 · (ℑ‘𝐴)) |
15 | | mulass 7905 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → ((i · i)
· (ℑ‘𝐴))
= (i · (i · (ℑ‘𝐴)))) |
16 | 5, 5, 15 | mp3an12 1322 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝐴)
∈ ℂ → ((i · i) · (ℑ‘𝐴)) = (i · (i ·
(ℑ‘𝐴)))) |
17 | 7, 16 | syl 14 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((i
· i) · (ℑ‘𝐴)) = (i · (i ·
(ℑ‘𝐴)))) |
18 | 7 | mulm1d 8329 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) |
19 | 14, 17, 18 | 3eqtr3a 2227 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· (i · (ℑ‘𝐴))) = -(ℑ‘𝐴)) |
20 | 19 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((i
· (ℜ‘𝐴))
+ (i · (i · (ℑ‘𝐴)))) = ((i · (ℜ‘𝐴)) + -(ℑ‘𝐴))) |
21 | 12, 20 | eqtrd 2203 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· ((ℜ‘𝐴)
+ (i · (ℑ‘𝐴)))) = ((i · (ℜ‘𝐴)) + -(ℑ‘𝐴))) |
22 | 2, 21 | eqtrd 2203 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) = ((i ·
(ℜ‘𝐴)) +
-(ℑ‘𝐴))) |
23 | 22 | fveq2d 5500 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= (exp‘((i · (ℜ‘𝐴)) + -(ℑ‘𝐴)))) |
24 | | mulcl 7901 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (i ·
(ℜ‘𝐴)) ∈
ℂ) |
25 | 5, 4, 24 | sylancr 412 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· (ℜ‘𝐴))
∈ ℂ) |
26 | 6 | renegcld 8299 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) |
27 | 26 | recnd 7948 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℂ) |
28 | | efadd 11638 |
. . . . . . 7
⊢ (((i
· (ℜ‘𝐴))
∈ ℂ ∧ -(ℑ‘𝐴) ∈ ℂ) → (exp‘((i
· (ℜ‘𝐴))
+ -(ℑ‘𝐴))) =
((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) |
29 | 25, 27, 28 | syl2anc 409 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘((i · (ℜ‘𝐴)) + -(ℑ‘𝐴))) = ((exp‘(i ·
(ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) |
30 | 23, 29 | eqtrd 2203 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) |
31 | 30 | eqeq1d 2179 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
= 1 ↔ ((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1)) |
32 | | efcl 11627 |
. . . . . . . . 9
⊢ ((i
· (ℜ‘𝐴))
∈ ℂ → (exp‘(i · (ℜ‘𝐴))) ∈ ℂ) |
33 | 25, 32 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘(i · (ℜ‘𝐴))) ∈ ℂ) |
34 | | efcl 11627 |
. . . . . . . . 9
⊢
(-(ℑ‘𝐴)
∈ ℂ → (exp‘-(ℑ‘𝐴)) ∈ ℂ) |
35 | 27, 34 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘-(ℑ‘𝐴)) ∈ ℂ) |
36 | 33, 35 | absmuld 11158 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(abs‘((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴)))) = ((abs‘(exp‘(i ·
(ℜ‘𝐴))))
· (abs‘(exp‘-(ℑ‘𝐴))))) |
37 | | absefi 11731 |
. . . . . . . . 9
⊢
((ℜ‘𝐴)
∈ ℝ → (abs‘(exp‘(i · (ℜ‘𝐴)))) = 1) |
38 | 3, 37 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘(i · (ℜ‘𝐴)))) = 1) |
39 | 26 | reefcld 11632 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘-(ℑ‘𝐴)) ∈ ℝ) |
40 | | efgt0 11647 |
. . . . . . . . . . 11
⊢
(-(ℑ‘𝐴)
∈ ℝ → 0 < (exp‘-(ℑ‘𝐴))) |
41 | 26, 40 | syl 14 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 0 <
(exp‘-(ℑ‘𝐴))) |
42 | | 0re 7920 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
43 | | ltle 8007 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (exp‘-(ℑ‘𝐴)) ∈ ℝ) → (0 <
(exp‘-(ℑ‘𝐴)) → 0 ≤
(exp‘-(ℑ‘𝐴)))) |
44 | 42, 43 | mpan 422 |
. . . . . . . . . 10
⊢
((exp‘-(ℑ‘𝐴)) ∈ ℝ → (0 <
(exp‘-(ℑ‘𝐴)) → 0 ≤
(exp‘-(ℑ‘𝐴)))) |
45 | 39, 41, 44 | sylc 62 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 0 ≤
(exp‘-(ℑ‘𝐴))) |
46 | 39, 45 | absidd 11131 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘-(ℑ‘𝐴))) = (exp‘-(ℑ‘𝐴))) |
47 | 38, 46 | oveq12d 5871 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((abs‘(exp‘(i · (ℜ‘𝐴)))) ·
(abs‘(exp‘-(ℑ‘𝐴)))) = (1 ·
(exp‘-(ℑ‘𝐴)))) |
48 | 35 | mulid2d 7938 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (1
· (exp‘-(ℑ‘𝐴))) = (exp‘-(ℑ‘𝐴))) |
49 | 36, 47, 48 | 3eqtrrd 2208 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘-(ℑ‘𝐴)) = (abs‘((exp‘(i ·
(ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))))) |
50 | | fveq2 5496 |
. . . . . 6
⊢
(((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1 → (abs‘((exp‘(i
· (ℜ‘𝐴)))
· (exp‘-(ℑ‘𝐴)))) = (abs‘1)) |
51 | 49, 50 | sylan9eq 2223 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1) →
(exp‘-(ℑ‘𝐴)) = (abs‘1)) |
52 | 51 | ex 114 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(((exp‘(i · (ℜ‘𝐴))) ·
(exp‘-(ℑ‘𝐴))) = 1 →
(exp‘-(ℑ‘𝐴)) = (abs‘1))) |
53 | 31, 52 | sylbid 149 |
. . 3
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
= 1 → (exp‘-(ℑ‘𝐴)) = (abs‘1))) |
54 | 7 | negeq0d 8222 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) = 0
↔ -(ℑ‘𝐴) =
0)) |
55 | | reim0b 10826 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
56 | | ef0 11635 |
. . . . . . 7
⊢
(exp‘0) = 1 |
57 | | abs1 11036 |
. . . . . . 7
⊢
(abs‘1) = 1 |
58 | 56, 57 | eqtr4i 2194 |
. . . . . 6
⊢
(exp‘0) = (abs‘1) |
59 | 58 | eqeq2i 2181 |
. . . . 5
⊢
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
(exp‘-(ℑ‘𝐴)) = (abs‘1)) |
60 | | reef11 11662 |
. . . . . 6
⊢
((-(ℑ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) |
61 | 26, 42, 60 | sylancl 411 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (exp‘0) ↔
-(ℑ‘𝐴) =
0)) |
62 | 59, 61 | bitr3id 193 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (abs‘1) ↔
-(ℑ‘𝐴) =
0)) |
63 | 54, 55, 62 | 3bitr4rd 220 |
. . 3
⊢ (𝐴 ∈ ℂ →
((exp‘-(ℑ‘𝐴)) = (abs‘1) ↔ 𝐴 ∈ ℝ)) |
64 | 53, 63 | sylibd 148 |
. 2
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
= 1 → 𝐴 ∈
ℝ)) |
65 | 64 | imp 123 |
1
⊢ ((𝐴 ∈ ℂ ∧
(exp‘(i · 𝐴))
= 1) → 𝐴 ∈
ℝ) |