Metamath Proof Explorer

Theorem sinval

Description: Value of the sine function. (Contributed by NM, 14-Mar-2005) (Revised by Mario Carneiro, 10-Nov-2013)

Ref Expression
Assertion sinval ${⊢}{A}\in ℂ\to \mathrm{sin}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2\mathrm{i}}$

Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}={A}\to \mathrm{i}{x}=\mathrm{i}{A}$
2 1 fveq2d ${⊢}{x}={A}\to {\mathrm{e}}^{\mathrm{i}{x}}={\mathrm{e}}^{\mathrm{i}{A}}$
3 oveq2 ${⊢}{x}={A}\to \left(-\mathrm{i}\right){x}=\left(-\mathrm{i}\right){A}$
4 3 fveq2d ${⊢}{x}={A}\to {\mathrm{e}}^{\left(-\mathrm{i}\right){x}}={\mathrm{e}}^{\left(-\mathrm{i}\right){A}}$
5 2 4 oveq12d ${⊢}{x}={A}\to {\mathrm{e}}^{\mathrm{i}{x}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}={\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}$
6 5 oveq1d ${⊢}{x}={A}\to \frac{{\mathrm{e}}^{\mathrm{i}{x}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}}{2\mathrm{i}}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2\mathrm{i}}$
7 df-sin ${⊢}\mathrm{sin}=\left({x}\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}{x}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}}{2\mathrm{i}}\right)$
8 ovex ${⊢}\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2\mathrm{i}}\in \mathrm{V}$
9 6 7 8 fvmpt ${⊢}{A}\in ℂ\to \mathrm{sin}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2\mathrm{i}}$