# 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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( abs ‘ 𝐴 ) = ( abs ‘ 𝐵 ) ) )

### Proof

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