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

Metamath Proof Explorer

Theorem efne0d

Description: The exponential of a complex number is nonzero, deduction form. (Contributed by NM, 13-Jan-2006) (Revised by Mario Carneiro, 29-Apr-2014) (Revised 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 )