Description: The exponential of a complex number is nonzero. Corollary 15-4.3 of Gleason p. 309. (Contributed by NM, 13-Jan-2006) (Revised by Mario Carneiro, 29-Apr-2014) (Proof shortened by TA, 14-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | efne0 | |- ( A e. CC -> ( exp ` A ) =/= 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( A e. CC -> A e. CC ) |
|
| 2 | 1 | efne0d | |- ( A e. CC -> ( exp ` A ) =/= 0 ) |