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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		neorian	⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
2	1	con2bii	⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) ↔ ¬ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
3		crne0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) )
4	3	necon2bbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) = 0 ↔ ¬ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) )
5	2 4	bitr4id	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) = 0 ) )