Theorem sumsqeq0

Description: The sum of two squres of reals is zero if and only if both reals are zero. (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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A=0\wedge B=0\right)\leftrightarrow A^2+B^2=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		resqcl	$$⊢A\in ℝ\to A^2\in ℝ$$
2		sqge0	$$⊢A\in ℝ\to 0\le A^2$$
3	1 2	jca	$$⊢A\in ℝ\to \left(A^2\in ℝ\wedge 0\le A^2\right)$$
4		resqcl	$$⊢B\in ℝ\to B^2\in ℝ$$
5		sqge0	$$⊢B\in ℝ\to 0\le B^2$$
6	4 5	jca	$$⊢B\in ℝ\to \left(B^2\in ℝ\wedge 0\le B^2\right)$$
7		add20	$$⊢\left(\left(A^2\in ℝ\wedge 0\le A^2\right)\wedge \left(B^2\in ℝ\wedge 0\le B^2\right)\right)\to \left(A^2+B^2=0\leftrightarrow \left(A^2=0\wedge B^2=0\right)\right)$$
8	3 6 7	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A^2+B^2=0\leftrightarrow \left(A^2=0\wedge B^2=0\right)\right)$$
9		recn	$$⊢A\in ℝ\to A\in ℂ$$
10		sqeq0	$$⊢A\in ℂ\to \left(A^2=0\leftrightarrow A=0\right)$$
11	9 10	syl	$$⊢A\in ℝ\to \left(A^2=0\leftrightarrow A=0\right)$$
12		recn	$$⊢B\in ℝ\to B\in ℂ$$
13		sqeq0	$$⊢B\in ℂ\to \left(B^2=0\leftrightarrow B=0\right)$$
14	12 13	syl	$$⊢B\in ℝ\to \left(B^2=0\leftrightarrow B=0\right)$$
15	11 14	bi2anan9	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A^2=0\wedge B^2=0\right)\leftrightarrow \left(A=0\wedge B=0\right)\right)$$
16	8 15	bitr2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A=0\wedge B=0\right)\leftrightarrow A^2+B^2=0\right)$$