Metamath Proof Explorer

Theorem sqabs

Description: The squares of two reals are equal iff their absolute values are equal. (Contributed by NM, 6-Mar-2009)

Ref Expression
Assertion sqabs ⊢ A ∈ ℝ ∧ B ∈ ℝ → A 2 = B 2 ↔ A = B

Proof

Step Hyp Ref Expression
1 resqcl ⊢ A ∈ ℝ → A 2 ∈ ℝ
2 sqge0 ⊢ A ∈ ℝ → 0 ≤ A 2
3 absid ⊢ A 2 ∈ ℝ ∧ 0 ≤ A 2 → A 2 = A 2
4 1 2 3 syl2anc ⊢ A ∈ ℝ → A 2 = A 2
5 recn ⊢ A ∈ ℝ → A ∈ ℂ
6 2nn0 ⊢ 2 ∈ ℕ 0
7 absexp ⊢ A ∈ ℂ ∧ 2 ∈ ℕ 0 → A 2 = A 2
8 5 6 7 sylancl ⊢ A ∈ ℝ → A 2 = A 2
9 4 8 eqtr3d ⊢ A ∈ ℝ → A 2 = A 2
10 resqcl ⊢ B ∈ ℝ → B 2 ∈ ℝ
11 sqge0 ⊢ B ∈ ℝ → 0 ≤ B 2
12 absid ⊢ B 2 ∈ ℝ ∧ 0 ≤ B 2 → B 2 = B 2
13 10 11 12 syl2anc ⊢ B ∈ ℝ → B 2 = B 2
14 recn ⊢ B ∈ ℝ → B ∈ ℂ
15 absexp ⊢ B ∈ ℂ ∧ 2 ∈ ℕ 0 → B 2 = B 2
16 14 6 15 sylancl ⊢ B ∈ ℝ → B 2 = B 2
17 13 16 eqtr3d ⊢ B ∈ ℝ → B 2 = B 2
18 9 17 eqeqan12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A 2 = B 2 ↔ A 2 = B 2
19 abscl ⊢ A ∈ ℂ → A ∈ ℝ
20 absge0 ⊢ A ∈ ℂ → 0 ≤ A
21 19 20 jca ⊢ A ∈ ℂ → A ∈ ℝ ∧ 0 ≤ A
22 abscl ⊢ B ∈ ℂ → B ∈ ℝ
23 absge0 ⊢ B ∈ ℂ → 0 ≤ B
24 22 23 jca ⊢ B ∈ ℂ → B ∈ ℝ ∧ 0 ≤ B
25 sq11 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 = B 2 ↔ A = B
26 21 24 25 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 = B 2 ↔ A = B
27 5 14 26 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A 2 = B 2 ↔ A = B
28 18 27 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A 2 = B 2 ↔ A = B