Theorem creq0

Description: The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 . (Contributed by Thierry Arnoux, 20-Aug-2023)

	Ref	Expression
Assertion	creq0	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A=0\wedge B=0\right)\leftrightarrow A+\mathrm{i}B=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		neorian	$$⊢\left(A\ne 0\vee B\ne 0\right)\leftrightarrow \neg \left(A=0\wedge B=0\right)$$
2	1	con2bii	$$⊢\left(A=0\wedge B=0\right)\leftrightarrow \neg \left(A\ne 0\vee B\ne 0\right)$$
3		crne0	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A\ne 0\vee B\ne 0\right)\leftrightarrow A+\mathrm{i}B\ne 0\right)$$
4	3	necon2bbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A+\mathrm{i}B=0\leftrightarrow \neg \left(A\ne 0\vee B\ne 0\right)\right)$$
5	2 4	bitr4id	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A=0\wedge B=0\right)\leftrightarrow A+\mathrm{i}B=0\right)$$