cjne0

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

		Ref	Expression
	Assertion	cjne0	$⊢ A \in ℂ \to (A \neq 0 \leftrightarrow \overline{A} \neq 0)$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		cj11	$⊢ (A \in ℂ \land 0 \in ℂ) \to (\overline{A} = \overline{0} \leftrightarrow A = 0)$
3	1 2	mpan2	$⊢ A \in ℂ \to (\overline{A} = \overline{0} \leftrightarrow A = 0)$
4		cj0	$⊢ \overline{0} = 0$
5	4	eqeq2i	$⊢ \overline{A} = \overline{0} \leftrightarrow \overline{A} = 0$
6	3 5	bitr3di	$⊢ A \in ℂ \to (A = 0 \leftrightarrow \overline{A} = 0)$
7	6	necon3bid	$⊢ A \in ℂ \to (A \neq 0 \leftrightarrow \overline{A} \neq 0)$

Metamath Proof Explorer