Metamath Proof Explorer


Theorem resinval

Description: The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion resinval ( ๐ด โˆˆ โ„ โ†’ ( sin โ€˜ ๐ด ) = ( โ„‘ โ€˜ ( exp โ€˜ ( i ยท ๐ด ) ) ) )

Proof

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 ยท ๐ด ) ) ) )