Detailed syntax breakdown of Definition df-sin
Step | Hyp | Ref
| Expression |
1 | | csin 15625 |
. 2
class
sin |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cc 10727 |
. . 3
class
ℂ |
4 | | ci 10731 |
. . . . . . 7
class
i |
5 | 2 | cv 1542 |
. . . . . . 7
class 𝑥 |
6 | | cmul 10734 |
. . . . . . 7
class
· |
7 | 4, 5, 6 | co 7213 |
. . . . . 6
class (i
· 𝑥) |
8 | | ce 15623 |
. . . . . 6
class
exp |
9 | 7, 8 | cfv 6380 |
. . . . 5
class
(exp‘(i · 𝑥)) |
10 | 4 | cneg 11063 |
. . . . . . 7
class
-i |
11 | 10, 5, 6 | co 7213 |
. . . . . 6
class (-i
· 𝑥) |
12 | 11, 8 | cfv 6380 |
. . . . 5
class
(exp‘(-i · 𝑥)) |
13 | | cmin 11062 |
. . . . 5
class
− |
14 | 9, 12, 13 | co 7213 |
. . . 4
class
((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) |
15 | | c2 11885 |
. . . . 5
class
2 |
16 | 15, 4, 6 | co 7213 |
. . . 4
class (2
· i) |
17 | | cdiv 11489 |
. . . 4
class
/ |
18 | 14, 16, 17 | co 7213 |
. . 3
class
(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 ·
i)) |
19 | 2, 3, 18 | cmpt 5135 |
. 2
class (𝑥 ∈ ℂ ↦
(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 ·
i))) |
20 | 1, 19 | wceq 1543 |
1
wff sin =
(𝑥 ∈ ℂ ↦
(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 ·
i))) |