Step |
Hyp |
Ref |
Expression |
1 |
|
recn |
โข ( ๐ด โ โ โ ๐ด โ โ ) |
2 |
|
recn |
โข ( ๐ต โ โ โ ๐ต โ โ ) |
3 |
|
efival |
โข ( ๐ด โ โ โ ( exp โ ( i ยท ๐ด ) ) = ( ( cos โ ๐ด ) + ( i ยท ( sin โ ๐ด ) ) ) ) |
4 |
|
efival |
โข ( ๐ต โ โ โ ( exp โ ( i ยท ๐ต ) ) = ( ( cos โ ๐ต ) + ( i ยท ( sin โ ๐ต ) ) ) ) |
5 |
3 4
|
eqeqan12d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( exp โ ( i ยท ๐ด ) ) = ( exp โ ( i ยท ๐ต ) ) โ ( ( cos โ ๐ด ) + ( i ยท ( sin โ ๐ด ) ) ) = ( ( cos โ ๐ต ) + ( i ยท ( sin โ ๐ต ) ) ) ) ) |
6 |
1 2 5
|
syl2an |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( exp โ ( i ยท ๐ด ) ) = ( exp โ ( i ยท ๐ต ) ) โ ( ( cos โ ๐ด ) + ( i ยท ( sin โ ๐ด ) ) ) = ( ( cos โ ๐ต ) + ( i ยท ( sin โ ๐ต ) ) ) ) ) |
7 |
|
recoscl |
โข ( ๐ด โ โ โ ( cos โ ๐ด ) โ โ ) |
8 |
|
resincl |
โข ( ๐ด โ โ โ ( sin โ ๐ด ) โ โ ) |
9 |
7 8
|
jca |
โข ( ๐ด โ โ โ ( ( cos โ ๐ด ) โ โ โง ( sin โ ๐ด ) โ โ ) ) |
10 |
|
recoscl |
โข ( ๐ต โ โ โ ( cos โ ๐ต ) โ โ ) |
11 |
|
resincl |
โข ( ๐ต โ โ โ ( sin โ ๐ต ) โ โ ) |
12 |
10 11
|
jca |
โข ( ๐ต โ โ โ ( ( cos โ ๐ต ) โ โ โง ( sin โ ๐ต ) โ โ ) ) |
13 |
|
cru |
โข ( ( ( ( cos โ ๐ด ) โ โ โง ( sin โ ๐ด ) โ โ ) โง ( ( cos โ ๐ต ) โ โ โง ( sin โ ๐ต ) โ โ ) ) โ ( ( ( cos โ ๐ด ) + ( i ยท ( sin โ ๐ด ) ) ) = ( ( cos โ ๐ต ) + ( i ยท ( sin โ ๐ต ) ) ) โ ( ( cos โ ๐ด ) = ( cos โ ๐ต ) โง ( sin โ ๐ด ) = ( sin โ ๐ต ) ) ) ) |
14 |
9 12 13
|
syl2an |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( ( cos โ ๐ด ) + ( i ยท ( sin โ ๐ด ) ) ) = ( ( cos โ ๐ต ) + ( i ยท ( sin โ ๐ต ) ) ) โ ( ( cos โ ๐ด ) = ( cos โ ๐ต ) โง ( sin โ ๐ด ) = ( sin โ ๐ต ) ) ) ) |
15 |
6 14
|
bitrd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( exp โ ( i ยท ๐ด ) ) = ( exp โ ( i ยท ๐ต ) ) โ ( ( cos โ ๐ด ) = ( cos โ ๐ต ) โง ( sin โ ๐ด ) = ( sin โ ๐ต ) ) ) ) |