Description: Closure law for the exponential function. (Contributed by NM, 8-Jan-2006) (Revised by Mario Carneiro, 10-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | efcl | ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eff | ⊢ exp : ℂ ⟶ ℂ | |
| 2 | 1 | ffvelcdmi | ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ ) |