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

Proof

Step	Hyp	Ref	Expression
1		resqcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )
2		sqge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 ↑ 2 ) )
3	1 2	jca	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) )
4		resqcl	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ↑ 2 ) ∈ ℝ )
5		sqge0	⊢ ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐵 ↑ 2 ) )
6	4 5	jca	⊢ ( 𝐵 ∈ ℝ → ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 ↑ 2 ) ) )
7		add20	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) ∧ ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 ↑ 2 ) ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( 𝐴 ↑ 2 ) = 0 ∧ ( 𝐵 ↑ 2 ) = 0 ) ) )
8	3 6 7	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( 𝐴 ↑ 2 ) = 0 ∧ ( 𝐵 ↑ 2 ) = 0 ) ) )
9		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
10		sqeq0	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) )
11	9 10	syl	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) )
12		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
13		sqeq0	⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 ↑ 2 ) = 0 ↔ 𝐵 = 0 ) )
14	12 13	syl	⊢ ( 𝐵 ∈ ℝ → ( ( 𝐵 ↑ 2 ) = 0 ↔ 𝐵 = 0 ) )
15	11 14	bi2anan9	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) = 0 ∧ ( 𝐵 ↑ 2 ) = 0 ) ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
16	8 15	bitr2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 0 ) )