This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efne0OLD

Description: Obsolete version of efne0 as of 14-Nov-2025. 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 modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion efne0OLD 
|- ( 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 )