Metamath Proof Explorer


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 A B A = 0 B = 0 A + i B = 0

Proof

Step Hyp Ref Expression
1 neorian A 0 B 0 ¬ A = 0 B = 0
2 1 con2bii A = 0 B = 0 ¬ A 0 B 0
3 crne0 A B A 0 B 0 A + i B 0
4 3 necon2bbid A B A + i B = 0 ¬ A 0 B 0
5 2 4 bitr4id A B A = 0 B = 0 A + i B = 0