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 \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	$$⊢\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 \sin A=\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2\mathrm{i}}$$