Definition df-sin

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

	Ref	Expression
Assertion	df-sin	⊢ sin = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csin	⊢ sin
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		ce	⊢ exp
4		ci	⊢ i
5		cmul	⊢ ·
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( i · 𝑥 )
8	7 3	cfv	⊢ ( exp ‘ ( i · 𝑥 ) )
9		cmin	⊢ −
10	4	cneg	⊢ - i
11	10 6 5	co	⊢ ( - i · 𝑥 )
12	11 3	cfv	⊢ ( exp ‘ ( - i · 𝑥 ) )
13	8 12 9	co	⊢ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) )
14		cdiv	⊢ /
15		c2	⊢ 2
16	15 4 5	co	⊢ ( 2 · i )
17	13 16 14	co	⊢ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) )
18	1 2 17	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) )
19	0 18	wceq	⊢ sin = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) )