Metamath Proof Explorer

Theorem crne0

Description: The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	crne0	$⊢ (A \in ℝ \land B \in ℝ) \to ((A \neq 0 \lor B \neq 0) \leftrightarrow A + i B \neq 0)$

Proof

Step	Hyp	Ref	Expression
1		neorian	$⊢ (A \neq 0 \lor B \neq 0) \leftrightarrow \neg (A = 0 \land B = 0)$
2		ax-icn	$⊢ i \in ℂ$
3	2	mul01i	$⊢ i \cdot 0 = 0$
4	3	oveq2i	$⊢ 0 + i \cdot 0 = 0 + 0$
5		00id	$⊢ 0 + 0 = 0$
6	4 5	eqtri	$⊢ 0 + i \cdot 0 = 0$
7	6	eqeq2i	$⊢ A + i B = 0 + i \cdot 0 \leftrightarrow A + i B = 0$
8		0re	$⊢ 0 \in ℝ$
9		cru	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \in ℝ \land 0 \in ℝ)) \to (A + i B = 0 + i \cdot 0 \leftrightarrow (A = 0 \land B = 0))$
10	8 8 9	mpanr12	$⊢ (A \in ℝ \land B \in ℝ) \to (A + i B = 0 + i \cdot 0 \leftrightarrow (A = 0 \land B = 0))$
11	7 10	bitr3id	$⊢ (A \in ℝ \land B \in ℝ) \to (A + i B = 0 \leftrightarrow (A = 0 \land B = 0))$
12	11	necon3abid	$⊢ (A \in ℝ \land B \in ℝ) \to (A + i B \neq 0 \leftrightarrow \neg (A = 0 \land B = 0))$
13	1 12	bitr4id	$⊢ (A \in ℝ \land B \in ℝ) \to ((A \neq 0 \lor B \neq 0) \leftrightarrow A + i B \neq 0)$