Metamath Proof Explorer


Theorem efne0

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)

Ref Expression
Assertion efne0
|- ( A e. CC -> ( exp ` A ) =/= 0 )

Proof

Step Hyp Ref Expression
1 ax-1ne0
 |-  1 =/= 0
2 oveq1
 |-  ( ( exp ` A ) = 0 -> ( ( exp ` A ) x. ( exp ` -u A ) ) = ( 0 x. ( exp ` -u A ) ) )
3 efcan
 |-  ( A e. CC -> ( ( exp ` A ) x. ( exp ` -u A ) ) = 1 )
4 negcl
 |-  ( A e. CC -> -u A e. CC )
5 efcl
 |-  ( -u A e. CC -> ( exp ` -u A ) e. CC )
6 4 5 syl
 |-  ( A e. CC -> ( exp ` -u A ) e. CC )
7 6 mul02d
 |-  ( A e. CC -> ( 0 x. ( exp ` -u A ) ) = 0 )
8 3 7 eqeq12d
 |-  ( A e. CC -> ( ( ( exp ` A ) x. ( exp ` -u A ) ) = ( 0 x. ( exp ` -u A ) ) <-> 1 = 0 ) )
9 2 8 syl5ib
 |-  ( A e. CC -> ( ( exp ` A ) = 0 -> 1 = 0 ) )
10 9 necon3d
 |-  ( A e. CC -> ( 1 =/= 0 -> ( exp ` A ) =/= 0 ) )
11 1 10 mpi
 |-  ( A e. CC -> ( exp ` A ) =/= 0 )