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