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 ) )