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 | ffvelrni | ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ ) |