Step |
Hyp |
Ref |
Expression |
1 |
|
recosval |
โข ( ๐ด โ โ โ ( cos โ ๐ด ) = ( โ โ ( exp โ ( i ยท ๐ด ) ) ) ) |
2 |
|
ax-icn |
โข i โ โ |
3 |
|
recn |
โข ( ๐ด โ โ โ ๐ด โ โ ) |
4 |
|
mulcl |
โข ( ( i โ โ โง ๐ด โ โ ) โ ( i ยท ๐ด ) โ โ ) |
5 |
2 3 4
|
sylancr |
โข ( ๐ด โ โ โ ( i ยท ๐ด ) โ โ ) |
6 |
|
efcl |
โข ( ( i ยท ๐ด ) โ โ โ ( exp โ ( i ยท ๐ด ) ) โ โ ) |
7 |
5 6
|
syl |
โข ( ๐ด โ โ โ ( exp โ ( i ยท ๐ด ) ) โ โ ) |
8 |
7
|
recld |
โข ( ๐ด โ โ โ ( โ โ ( exp โ ( i ยท ๐ด ) ) ) โ โ ) |
9 |
1 8
|
eqeltrd |
โข ( ๐ด โ โ โ ( cos โ ๐ด ) โ โ ) |