Definition df-sin

Description: Define the sine function. (Contributed by NM, 14-Mar-2005)

	Ref	Expression
Assertion	df-sin	$$⊢\sin =\left(x\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csin	$$class\sin$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		ce	$$class\exp$$
4		ci	$$class\mathrm{i}$$
5		cmul	$$class\times$$
6	1	cv	$$setvarx$$
7	4 6 5	co	$$class\mathrm{i}x$$
8	7 3	cfv	$$class{\mathrm{e}}^{\mathrm{i}x}$$
9		cmin	$$class-$$
10	4	cneg	$$class\left(-\mathrm{i}\right)$$
11	10 6 5	co	$$class\left(-\mathrm{i}\right)x$$
12	11 3	cfv	$$class{\mathrm{e}}^{\left(-\mathrm{i}\right)x}$$
13	8 12 9	co	$$class\left({\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}\right)$$
14		cdiv	$$class÷$$
15		c2	$$class2$$
16	15 4 5	co	$$class2\mathrm{i}$$
17	13 16 14	co	$$class\left(\frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\right)$$
18	1 2 17	cmpt	$$class\left(x\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\right)$$
19	0 18	wceq	$$wff\sin =\left(x\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\right)$$