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	imbitrid	|- ( 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 )