Description: A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | cjne0 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 ↔ ( ∗ ‘ 𝐴 ) ≠ 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cj0 | ⊢ ( ∗ ‘ 0 ) = 0 | |
2 | 1 | eqeq2i | ⊢ ( ( ∗ ‘ 𝐴 ) = ( ∗ ‘ 0 ) ↔ ( ∗ ‘ 𝐴 ) = 0 ) |
3 | 0cn | ⊢ 0 ∈ ℂ | |
4 | cj11 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) = ( ∗ ‘ 0 ) ↔ 𝐴 = 0 ) ) | |
5 | 3 4 | mpan2 | ⊢ ( 𝐴 ∈ ℂ → ( ( ∗ ‘ 𝐴 ) = ( ∗ ‘ 0 ) ↔ 𝐴 = 0 ) ) |
6 | 2 5 | syl5rbbr | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 = 0 ↔ ( ∗ ‘ 𝐴 ) = 0 ) ) |
7 | 6 | necon3bid | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 ↔ ( ∗ ‘ 𝐴 ) ≠ 0 ) ) |