Proof of Theorem efival
Step | Hyp | Ref
| Expression |
1 | | ax-icn 10396 |
. . . . . 6
⊢ i ∈
ℂ |
2 | | mulcl 10421 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
3 | 1, 2 | mpan 677 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) |
4 | | efcl 15299 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
∈ ℂ) |
6 | | negicn 10689 |
. . . . . 6
⊢ -i ∈
ℂ |
7 | | mulcl 10421 |
. . . . . 6
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
8 | 6, 7 | mpan 677 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (-i
· 𝐴) ∈
ℂ) |
9 | | efcl 15299 |
. . . . 5
⊢ ((-i
· 𝐴) ∈ ℂ
→ (exp‘(-i · 𝐴)) ∈ ℂ) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(exp‘(-i · 𝐴))
∈ ℂ) |
11 | 5, 10 | addcld 10461 |
. . 3
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))) ∈ ℂ) |
12 | 5, 10 | subcld 10800 |
. . 3
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
− (exp‘(-i · 𝐴))) ∈ ℂ) |
13 | | 2cn 11518 |
. . . . 5
⊢ 2 ∈
ℂ |
14 | | 2ne0 11554 |
. . . . 5
⊢ 2 ≠
0 |
15 | 13, 14 | pm3.2i 463 |
. . . 4
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
16 | | divdir 11126 |
. . . 4
⊢
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ ∧
((exp‘(i · 𝐴))
− (exp‘(-i · 𝐴))) ∈ ℂ ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴)))) / 2) =
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) / 2))) |
17 | 15, 16 | mp3an3 1429 |
. . 3
⊢
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ ∧
((exp‘(i · 𝐴))
− (exp‘(-i · 𝐴))) ∈ ℂ) → ((((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) + ((exp‘(i · 𝐴)) − (exp‘(-i
· 𝐴)))) / 2) =
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) / 2))) |
18 | 11, 12, 17 | syl2anc 576 |
. 2
⊢ (𝐴 ∈ ℂ →
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴)))) / 2) =
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) / 2))) |
19 | 10, 5 | pncan3d 10803 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((exp‘(-i · 𝐴)) + ((exp‘(i · 𝐴)) − (exp‘(-i
· 𝐴)))) =
(exp‘(i · 𝐴))) |
20 | 19 | oveq2d 6994 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((exp‘(i · 𝐴))
+ ((exp‘(-i · 𝐴)) + ((exp‘(i · 𝐴)) − (exp‘(-i
· 𝐴))))) =
((exp‘(i · 𝐴))
+ (exp‘(i · 𝐴)))) |
21 | 5, 10, 12 | addassd 10464 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴)))) =
((exp‘(i · 𝐴))
+ ((exp‘(-i · 𝐴)) + ((exp‘(i · 𝐴)) − (exp‘(-i
· 𝐴)))))) |
22 | 5 | 2timesd 11693 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (2
· (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) + (exp‘(i ·
𝐴)))) |
23 | 20, 21, 22 | 3eqtr4d 2824 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴)))) = (2
· (exp‘(i · 𝐴)))) |
24 | 23 | oveq1d 6993 |
. . 3
⊢ (𝐴 ∈ ℂ →
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴)))) / 2) = ((2
· (exp‘(i · 𝐴))) / 2)) |
25 | | divcan3 11127 |
. . . . 5
⊢
(((exp‘(i · 𝐴)) ∈ ℂ ∧ 2 ∈ ℂ
∧ 2 ≠ 0) → ((2 · (exp‘(i · 𝐴))) / 2) = (exp‘(i · 𝐴))) |
26 | 13, 14, 25 | mp3an23 1432 |
. . . 4
⊢
((exp‘(i · 𝐴)) ∈ ℂ → ((2 ·
(exp‘(i · 𝐴)))
/ 2) = (exp‘(i · 𝐴))) |
27 | 5, 26 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℂ → ((2
· (exp‘(i · 𝐴))) / 2) = (exp‘(i · 𝐴))) |
28 | 24, 27 | eqtr2d 2815 |
. 2
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) + ((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴)))) /
2)) |
29 | | cosval 15339 |
. . 3
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) |
30 | | 2mulicn 11673 |
. . . . . . 7
⊢ (2
· i) ∈ ℂ |
31 | | 2muline0 11674 |
. . . . . . 7
⊢ (2
· i) ≠ 0 |
32 | 30, 31 | pm3.2i 463 |
. . . . . 6
⊢ ((2
· i) ∈ ℂ ∧ (2 · i) ≠ 0) |
33 | | div12 11123 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ ∧ ((2
· i) ∈ ℂ ∧ (2 · i) ≠ 0)) → (i ·
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 ·
i)))) |
34 | 1, 32, 33 | mp3an13 1431 |
. . . . 5
⊢
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ → (i
· (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 ·
i)))) |
35 | 12, 34 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℂ → (i
· (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 ·
i)))) |
36 | | sinval 15338 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i))) |
37 | 36 | oveq2d 6994 |
. . . 4
⊢ (𝐴 ∈ ℂ → (i
· (sin‘𝐴)) =
(i · (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i)))) |
38 | | divrec 11117 |
. . . . . . 7
⊢
((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 ≠ 0) → (((exp‘(i · 𝐴)) − (exp‘(-i
· 𝐴))) / 2) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (1 /
2))) |
39 | 13, 14, 38 | mp3an23 1432 |
. . . . . 6
⊢
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ →
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2) = (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) · (1 / 2))) |
40 | 12, 39 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2) = (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) · (1 / 2))) |
41 | 1 | mulid2i 10447 |
. . . . . . . 8
⊢ (1
· i) = i |
42 | 41 | oveq1i 6988 |
. . . . . . 7
⊢ ((1
· i) / (2 · i)) = (i / (2 · i)) |
43 | | ine0 10878 |
. . . . . . . . . . 11
⊢ i ≠
0 |
44 | 1, 43 | dividi 11176 |
. . . . . . . . . 10
⊢ (i / i) =
1 |
45 | 44 | oveq2i 6989 |
. . . . . . . . 9
⊢ ((1 / 2)
· (i / i)) = ((1 / 2) · 1) |
46 | | ax-1cn 10395 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
47 | 46, 13, 1, 1, 14, 43 | divmuldivi 11203 |
. . . . . . . . 9
⊢ ((1 / 2)
· (i / i)) = ((1 · i) / (2 · i)) |
48 | 45, 47 | eqtr3i 2804 |
. . . . . . . 8
⊢ ((1 / 2)
· 1) = ((1 · i) / (2 · i)) |
49 | | halfcn 11665 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℂ |
50 | 49 | mulid1i 10446 |
. . . . . . . 8
⊢ ((1 / 2)
· 1) = (1 / 2) |
51 | 48, 50 | eqtr3i 2804 |
. . . . . . 7
⊢ ((1
· i) / (2 · i)) = (1 / 2) |
52 | 42, 51 | eqtr3i 2804 |
. . . . . 6
⊢ (i / (2
· i)) = (1 / 2) |
53 | 52 | oveq2i 6989 |
. . . . 5
⊢
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (i / (2 ·
i))) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) · (1 /
2)) |
54 | 40, 53 | syl6eqr 2832 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2) = (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) · (i / (2 ·
i)))) |
55 | 35, 37, 54 | 3eqtr4d 2824 |
. . 3
⊢ (𝐴 ∈ ℂ → (i
· (sin‘𝐴)) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / 2)) |
56 | 29, 55 | oveq12d 6996 |
. 2
⊢ (𝐴 ∈ ℂ →
((cos‘𝐴) + (i
· (sin‘𝐴))) =
((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) + (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) / 2))) |
57 | 18, 28, 56 | 3eqtr4d 2824 |
1
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |