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

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	⊢ 1 ≠ 0
2		oveq1	⊢ ( ( exp ‘ 𝐴 ) = 0 → ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = ( 0 · ( exp ‘ - 𝐴 ) ) )
3		efcan	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = 1 )
4		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
5		efcl	⊢ ( - 𝐴 ∈ ℂ → ( exp ‘ - 𝐴 ) ∈ ℂ )
6	4 5	syl	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - 𝐴 ) ∈ ℂ )
7	6	mul02d	⊢ ( 𝐴 ∈ ℂ → ( 0 · ( exp ‘ - 𝐴 ) ) = 0 )
8	3 7	eqeq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = ( 0 · ( exp ‘ - 𝐴 ) ) ↔ 1 = 0 ) )
9	2 8	syl5ib	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) = 0 → 1 = 0 ) )
10	9	necon3d	⊢ ( 𝐴 ∈ ℂ → ( 1 ≠ 0 → ( exp ‘ 𝐴 ) ≠ 0 ) )
11	1 10	mpi	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ≠ 0 )