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 e. RR /\ B e. RR ) -> ( ( A = 0 /\ B = 0 ) <-> ( A + ( _i x. 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 e. RR /\ B e. RR ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 ) )
4	3	necon2bbid	|- ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) = 0 <-> -. ( A =/= 0 \/ B =/= 0 ) ) )
5	2 4	bitr4id	|- ( ( A e. RR /\ B e. RR ) -> ( ( A = 0 /\ B = 0 ) <-> ( A + ( _i x. B ) ) = 0 ) )