Detailed syntax breakdown of Definition df-cos
Step | Hyp | Ref
| Expression |
1 | | ccos 14634 |
. 2
class
cos |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cc 9813 |
. . 3
class
ℂ |
4 | | ci 9817 |
. . . . . . 7
class
i |
5 | 2 | cv 1474 |
. . . . . . 7
class 𝑥 |
6 | | cmul 9820 |
. . . . . . 7
class
· |
7 | 4, 5, 6 | co 6549 |
. . . . . 6
class (i
· 𝑥) |
8 | | ce 14631 |
. . . . . 6
class
exp |
9 | 7, 8 | cfv 5804 |
. . . . 5
class
(exp‘(i · 𝑥)) |
10 | 4 | cneg 10146 |
. . . . . . 7
class
-i |
11 | 10, 5, 6 | co 6549 |
. . . . . 6
class (-i
· 𝑥) |
12 | 11, 8 | cfv 5804 |
. . . . 5
class
(exp‘(-i · 𝑥)) |
13 | | caddc 9818 |
. . . . 5
class
+ |
14 | 9, 12, 13 | co 6549 |
. . . 4
class
((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) |
15 | | c2 10947 |
. . . 4
class
2 |
16 | | cdiv 10563 |
. . . 4
class
/ |
17 | 14, 15, 16 | co 6549 |
. . 3
class
(((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2) |
18 | 2, 3, 17 | cmpt 4643 |
. 2
class (𝑥 ∈ ℂ ↦
(((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2)) |
19 | 1, 18 | wceq 1475 |
1
wff cos =
(𝑥 ∈ ℂ ↦
(((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2)) |