Theorem sumsqeq0

Description: Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed by NM, 29-Apr-2005) (Revised by Stefan O'Rear, 5-Oct-2014) (Proof shortened by Mario Carneiro, 28-May-2016)

	Ref	Expression
Assertion	sumsqeq0	|- ( ( A e. RR /\ B e. RR ) -> ( ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		resqcl	|- ( A e. RR -> ( A ^ 2 ) e. RR )
2		sqge0	|- ( A e. RR -> 0 <_ ( A ^ 2 ) )
3	1 2	jca	|- ( A e. RR -> ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) )
4		resqcl	|- ( B e. RR -> ( B ^ 2 ) e. RR )
5		sqge0	|- ( B e. RR -> 0 <_ ( B ^ 2 ) )
6	4 5	jca	|- ( B e. RR -> ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) )
7		add20	|- ( ( ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) /\ ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 <-> ( ( A ^ 2 ) = 0 /\ ( B ^ 2 ) = 0 ) ) )
8	3 6 7	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 <-> ( ( A ^ 2 ) = 0 /\ ( B ^ 2 ) = 0 ) ) )
9		recn	|- ( A e. RR -> A e. CC )
10		sqeq0	|- ( A e. CC -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )
11	9 10	syl	|- ( A e. RR -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )
12		recn	|- ( B e. RR -> B e. CC )
13		sqeq0	|- ( B e. CC -> ( ( B ^ 2 ) = 0 <-> B = 0 ) )
14	12 13	syl	|- ( B e. RR -> ( ( B ^ 2 ) = 0 <-> B = 0 ) )
15	11 14	bi2anan9	|- ( ( A e. RR /\ B e. RR ) -> ( ( ( A ^ 2 ) = 0 /\ ( B ^ 2 ) = 0 ) <-> ( A = 0 /\ B = 0 ) ) )
16	8 15	bitr2d	|- ( ( A e. RR /\ B e. RR ) -> ( ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 ) )