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