Description: Define the exponential function. Its value at the complex number A is ( expA ) and is called the "exponential of A "; see efval . (Contributed by NM, 14-Mar-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | df-ef | |- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ce | |- exp |
|
1 | vx | |- x |
|
2 | cc | |- CC |
|
3 | vk | |- k |
|
4 | cn0 | |- NN0 |
|
5 | 1 | cv | |- x |
6 | cexp | |- ^ |
|
7 | 3 | cv | |- k |
8 | 5 7 6 | co | |- ( x ^ k ) |
9 | cdiv | |- / |
|
10 | cfa | |- ! |
|
11 | 7 10 | cfv | |- ( ! ` k ) |
12 | 8 11 9 | co | |- ( ( x ^ k ) / ( ! ` k ) ) |
13 | 4 12 3 | csu | |- sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) |
14 | 1 2 13 | cmpt | |- ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) ) |
15 | 0 14 | wceq | |- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) ) |