Metamath Proof Explorer

Definition df-sin

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

Ref Expression
Assertion df-sin ⊢ sin = x ∈ ℂ ⟼ e i ⁢ x − e − i ⁢ x 2 ⁢ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 csin class sin
1 vx setvar x
2 cc class ℂ
3 ce class exp
4 ci class i
5 cmul class ×
6 1 cv setvar x
7 4 6 5 co class i ⁢ x
8 7 3 cfv class e i ⁢ x
9 cmin class −
10 4 cneg class − i
11 10 6 5 co class − i ⁢ x
12 11 3 cfv class e − i ⁢ x
13 8 12 9 co class e i ⁢ x − e − i ⁢ x
14 cdiv class ÷
15 c2 class 2
16 15 4 5 co class 2 ⁢ i
17 13 16 14 co class e i ⁢ x − e − i ⁢ x 2 ⁢ i
18 1 2 17 cmpt class x ∈ ℂ ⟼ e i ⁢ x − e − i ⁢ x 2 ⁢ i
19 0 18 wceq wff sin = x ∈ ℂ ⟼ e i ⁢ x − e − i ⁢ x 2 ⁢ i