Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ef | Structured version Visualization version GIF version |
Description: Define the exponential function. Its value at the complex number 𝐴 is (exp‘𝐴) and is called the "exponential of 𝐴"; see efval 15834. (Contributed by NM, 14-Mar-2005.) |
Ref | Expression |
---|---|
df-ef | ⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ce 15816 | . 2 class exp | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cc 10915 | . . 3 class ℂ | |
4 | cn0 12279 | . . . 4 class ℕ0 | |
5 | 2 | cv 1538 | . . . . . 6 class 𝑥 |
6 | vk | . . . . . . 7 setvar 𝑘 | |
7 | 6 | cv 1538 | . . . . . 6 class 𝑘 |
8 | cexp 13828 | . . . . . 6 class ↑ | |
9 | 5, 7, 8 | co 7307 | . . . . 5 class (𝑥↑𝑘) |
10 | cfa 14033 | . . . . . 6 class ! | |
11 | 7, 10 | cfv 6458 | . . . . 5 class (!‘𝑘) |
12 | cdiv 11678 | . . . . 5 class / | |
13 | 9, 11, 12 | co 7307 | . . . 4 class ((𝑥↑𝑘) / (!‘𝑘)) |
14 | 4, 13, 6 | csu 15442 | . . 3 class Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘)) |
15 | 2, 3, 14 | cmpt 5164 | . 2 class (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) |
16 | 1, 15 | wceq 1539 | 1 wff exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) |
Colors of variables: wff setvar class |
This definition is referenced by: efval 15834 eff 15836 |
Copyright terms: Public domain | W3C validator |