This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐵 ) ) )