Metamath Proof Explorer

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 ∈ ℝ ∧ B ∈ ℝ → A = 0 ∧ B = 0 ↔ A 2 + B 2 = 0

Proof

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