(related to Corollary: Representing Real Sine by Complex Exponential Function)
By definition of the sine function of a real variable, we have \[\sin(x)=\Im(\exp(ix)),\quad\quad x\in\mathbb R.\]
From the formula of extracting the real part from a complex number, we get the result
\[\sin(x)=\Im(\exp(ix))=\frac 1{2i}(\exp(ix)-(\exp(ix))^*),\quad\quad x\in\mathbb R.\]
By the formula for calculating the complex conjugate of the complex exponential function, it follows
\[\sin(x)=\frac 1{2i}(\exp(ix)-\exp((ix)^*),\quad\quad x\in\mathbb R.\]
The definition of the complex conjugate leads to the desired result:
\[\sin(x)=\frac 1{2i}(\exp(ix)-\exp(-ix)),\quad\quad x\in\mathbb R.\]
