Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
โข i โ โ |
2 |
|
mulcl |
โข ( ( i โ โ โง ๐ด โ โ ) โ ( i ยท ๐ด ) โ โ ) |
3 |
1 2
|
mpan |
โข ( ๐ด โ โ โ ( i ยท ๐ด ) โ โ ) |
4 |
|
cosval |
โข ( ( i ยท ๐ด ) โ โ โ ( cos โ ( i ยท ๐ด ) ) = ( ( ( exp โ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ ( - i ยท ( i ยท ๐ด ) ) ) ) / 2 ) ) |
5 |
3 4
|
syl |
โข ( ๐ด โ โ โ ( cos โ ( i ยท ๐ด ) ) = ( ( ( exp โ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ ( - i ยท ( i ยท ๐ด ) ) ) ) / 2 ) ) |
6 |
|
negcl |
โข ( ๐ด โ โ โ - ๐ด โ โ ) |
7 |
|
efcl |
โข ( - ๐ด โ โ โ ( exp โ - ๐ด ) โ โ ) |
8 |
6 7
|
syl |
โข ( ๐ด โ โ โ ( exp โ - ๐ด ) โ โ ) |
9 |
|
efcl |
โข ( ๐ด โ โ โ ( exp โ ๐ด ) โ โ ) |
10 |
|
ixi |
โข ( i ยท i ) = - 1 |
11 |
10
|
oveq1i |
โข ( ( i ยท i ) ยท ๐ด ) = ( - 1 ยท ๐ด ) |
12 |
|
mulass |
โข ( ( i โ โ โง i โ โ โง ๐ด โ โ ) โ ( ( i ยท i ) ยท ๐ด ) = ( i ยท ( i ยท ๐ด ) ) ) |
13 |
1 1 12
|
mp3an12 |
โข ( ๐ด โ โ โ ( ( i ยท i ) ยท ๐ด ) = ( i ยท ( i ยท ๐ด ) ) ) |
14 |
|
mulm1 |
โข ( ๐ด โ โ โ ( - 1 ยท ๐ด ) = - ๐ด ) |
15 |
11 13 14
|
3eqtr3a |
โข ( ๐ด โ โ โ ( i ยท ( i ยท ๐ด ) ) = - ๐ด ) |
16 |
15
|
fveq2d |
โข ( ๐ด โ โ โ ( exp โ ( i ยท ( i ยท ๐ด ) ) ) = ( exp โ - ๐ด ) ) |
17 |
1 1
|
mulneg1i |
โข ( - i ยท i ) = - ( i ยท i ) |
18 |
10
|
negeqi |
โข - ( i ยท i ) = - - 1 |
19 |
|
negneg1e1 |
โข - - 1 = 1 |
20 |
17 18 19
|
3eqtri |
โข ( - i ยท i ) = 1 |
21 |
20
|
oveq1i |
โข ( ( - i ยท i ) ยท ๐ด ) = ( 1 ยท ๐ด ) |
22 |
|
negicn |
โข - i โ โ |
23 |
|
mulass |
โข ( ( - i โ โ โง i โ โ โง ๐ด โ โ ) โ ( ( - i ยท i ) ยท ๐ด ) = ( - i ยท ( i ยท ๐ด ) ) ) |
24 |
22 1 23
|
mp3an12 |
โข ( ๐ด โ โ โ ( ( - i ยท i ) ยท ๐ด ) = ( - i ยท ( i ยท ๐ด ) ) ) |
25 |
|
mulid2 |
โข ( ๐ด โ โ โ ( 1 ยท ๐ด ) = ๐ด ) |
26 |
21 24 25
|
3eqtr3a |
โข ( ๐ด โ โ โ ( - i ยท ( i ยท ๐ด ) ) = ๐ด ) |
27 |
26
|
fveq2d |
โข ( ๐ด โ โ โ ( exp โ ( - i ยท ( i ยท ๐ด ) ) ) = ( exp โ ๐ด ) ) |
28 |
16 27
|
oveq12d |
โข ( ๐ด โ โ โ ( ( exp โ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ ( - i ยท ( i ยท ๐ด ) ) ) ) = ( ( exp โ - ๐ด ) + ( exp โ ๐ด ) ) ) |
29 |
8 9 28
|
comraddd |
โข ( ๐ด โ โ โ ( ( exp โ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ ( - i ยท ( i ยท ๐ด ) ) ) ) = ( ( exp โ ๐ด ) + ( exp โ - ๐ด ) ) ) |
30 |
29
|
oveq1d |
โข ( ๐ด โ โ โ ( ( ( exp โ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ ( - i ยท ( i ยท ๐ด ) ) ) ) / 2 ) = ( ( ( exp โ ๐ด ) + ( exp โ - ๐ด ) ) / 2 ) ) |
31 |
5 30
|
eqtrd |
โข ( ๐ด โ โ โ ( cos โ ( i ยท ๐ด ) ) = ( ( ( exp โ ๐ด ) + ( exp โ - ๐ด ) ) / 2 ) ) |