Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
โข i โ โ |
2 |
|
recn |
โข ( ๐ด โ โ โ ๐ด โ โ ) |
3 |
|
cjmul |
โข ( ( i โ โ โง ๐ด โ โ ) โ ( โ โ ( i ยท ๐ด ) ) = ( ( โ โ i ) ยท ( โ โ ๐ด ) ) ) |
4 |
1 2 3
|
sylancr |
โข ( ๐ด โ โ โ ( โ โ ( i ยท ๐ด ) ) = ( ( โ โ i ) ยท ( โ โ ๐ด ) ) ) |
5 |
|
cji |
โข ( โ โ i ) = - i |
6 |
5
|
oveq1i |
โข ( ( โ โ i ) ยท ( โ โ ๐ด ) ) = ( - i ยท ( โ โ ๐ด ) ) |
7 |
|
cjre |
โข ( ๐ด โ โ โ ( โ โ ๐ด ) = ๐ด ) |
8 |
7
|
oveq2d |
โข ( ๐ด โ โ โ ( - i ยท ( โ โ ๐ด ) ) = ( - i ยท ๐ด ) ) |
9 |
6 8
|
eqtrid |
โข ( ๐ด โ โ โ ( ( โ โ i ) ยท ( โ โ ๐ด ) ) = ( - i ยท ๐ด ) ) |
10 |
4 9
|
eqtrd |
โข ( ๐ด โ โ โ ( โ โ ( i ยท ๐ด ) ) = ( - i ยท ๐ด ) ) |
11 |
10
|
fveq2d |
โข ( ๐ด โ โ โ ( exp โ ( โ โ ( i ยท ๐ด ) ) ) = ( exp โ ( - i ยท ๐ด ) ) ) |
12 |
|
mulcl |
โข ( ( i โ โ โง ๐ด โ โ ) โ ( i ยท ๐ด ) โ โ ) |
13 |
1 2 12
|
sylancr |
โข ( ๐ด โ โ โ ( i ยท ๐ด ) โ โ ) |
14 |
|
efcj |
โข ( ( i ยท ๐ด ) โ โ โ ( exp โ ( โ โ ( i ยท ๐ด ) ) ) = ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) |
15 |
13 14
|
syl |
โข ( ๐ด โ โ โ ( exp โ ( โ โ ( i ยท ๐ด ) ) ) = ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) |
16 |
11 15
|
eqtr3d |
โข ( ๐ด โ โ โ ( exp โ ( - i ยท ๐ด ) ) = ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) |
17 |
16
|
oveq2d |
โข ( ๐ด โ โ โ ( ( exp โ ( i ยท ๐ด ) ) โ ( exp โ ( - i ยท ๐ด ) ) ) = ( ( exp โ ( i ยท ๐ด ) ) โ ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) ) |
18 |
17
|
oveq1d |
โข ( ๐ด โ โ โ ( ( ( exp โ ( i ยท ๐ด ) ) โ ( exp โ ( - i ยท ๐ด ) ) ) / ( 2 ยท i ) ) = ( ( ( exp โ ( i ยท ๐ด ) ) โ ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) / ( 2 ยท i ) ) ) |
19 |
|
sinval |
โข ( ๐ด โ โ โ ( sin โ ๐ด ) = ( ( ( exp โ ( i ยท ๐ด ) ) โ ( exp โ ( - i ยท ๐ด ) ) ) / ( 2 ยท i ) ) ) |
20 |
2 19
|
syl |
โข ( ๐ด โ โ โ ( sin โ ๐ด ) = ( ( ( exp โ ( i ยท ๐ด ) ) โ ( exp โ ( - i ยท ๐ด ) ) ) / ( 2 ยท i ) ) ) |
21 |
|
efcl |
โข ( ( i ยท ๐ด ) โ โ โ ( exp โ ( i ยท ๐ด ) ) โ โ ) |
22 |
|
imval2 |
โข ( ( exp โ ( i ยท ๐ด ) ) โ โ โ ( โ โ ( exp โ ( i ยท ๐ด ) ) ) = ( ( ( exp โ ( i ยท ๐ด ) ) โ ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) / ( 2 ยท i ) ) ) |
23 |
13 21 22
|
3syl |
โข ( ๐ด โ โ โ ( โ โ ( exp โ ( i ยท ๐ด ) ) ) = ( ( ( exp โ ( i ยท ๐ด ) ) โ ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) / ( 2 ยท i ) ) ) |
24 |
18 20 23
|
3eqtr4d |
โข ( ๐ด โ โ โ ( sin โ ๐ด ) = ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) |