Theorem efne0d

Description: The exponential of a complex number is nonzero, deduction form. EDITORIAL: Using efne0d in efne0 is shorter than vice versa. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypothesis	efne0d.1	|- ( ph -> A e. CC )
Assertion	efne0d	|- ( ph -> ( exp ` A ) =/= 0 )

Proof

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