Metamath Proof Explorer

Theorem cjne0

Description: A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005)

Ref Expression
Assertion cjne0 
|- ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 cj11 
 |-  ( ( A e. CC /\ 0 e. CC ) -> ( ( * ` A ) = ( * ` 0 ) <-> A = 0 ) )
3 1 2 mpan2 
 |-  ( A e. CC -> ( ( * ` A ) = ( * ` 0 ) <-> A = 0 ) )
4 cj0 
 |-  ( * ` 0 ) = 0
5 4 eqeq2i 
 |-  ( ( * ` A ) = ( * ` 0 ) <-> ( * ` A ) = 0 )
6 3 5 bitr3di 
 |-  ( A e. CC -> ( A = 0 <-> ( * ` A ) = 0 ) )
7 6 necon3bid 
 |-  ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )