Metamath Proof Explorer


Theorem efieq

Description: The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion efieq ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( exp โ€˜ ( i ยท ๐ด ) ) = ( exp โ€˜ ( i ยท ๐ต ) ) โ†” ( ( cos โ€˜ ๐ด ) = ( cos โ€˜ ๐ต ) โˆง ( sin โ€˜ ๐ด ) = ( sin โ€˜ ๐ต ) ) ) )

Proof

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 โ€˜ ๐ต ) ) ) )