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 e. RR /\ B e. RR ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( abs ` A ) = ( abs ` B ) ) )

Proof

Step Hyp Ref Expression
1 resqcl 
 |-  ( A e. RR -> ( A ^ 2 ) e. RR )
2 sqge0 
 |-  ( A e. RR -> 0 <_ ( A ^ 2 ) )
3 absid 
 |-  ( ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) -> ( abs ` ( A ^ 2 ) ) = ( A ^ 2 ) )
4 1 2 3 syl2anc 
 |-  ( A e. RR -> ( abs ` ( A ^ 2 ) ) = ( A ^ 2 ) )
5 recn 
 |-  ( A e. RR -> A e. CC )
6 2nn0 
 |-  2 e. NN0
7 absexp 
 |-  ( ( A e. CC /\ 2 e. NN0 ) -> ( abs ` ( A ^ 2 ) ) = ( ( abs ` A ) ^ 2 ) )
8 5 6 7 sylancl 
 |-  ( A e. RR -> ( abs ` ( A ^ 2 ) ) = ( ( abs ` A ) ^ 2 ) )
9 4 8 eqtr3d 
 |-  ( A e. RR -> ( A ^ 2 ) = ( ( abs ` A ) ^ 2 ) )
10 resqcl 
 |-  ( B e. RR -> ( B ^ 2 ) e. RR )
11 sqge0 
 |-  ( B e. RR -> 0 <_ ( B ^ 2 ) )
12 absid 
 |-  ( ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) -> ( abs ` ( B ^ 2 ) ) = ( B ^ 2 ) )
13 10 11 12 syl2anc 
 |-  ( B e. RR -> ( abs ` ( B ^ 2 ) ) = ( B ^ 2 ) )
14 recn 
 |-  ( B e. RR -> B e. CC )
15 absexp 
 |-  ( ( B e. CC /\ 2 e. NN0 ) -> ( abs ` ( B ^ 2 ) ) = ( ( abs ` B ) ^ 2 ) )
16 14 6 15 sylancl 
 |-  ( B e. RR -> ( abs ` ( B ^ 2 ) ) = ( ( abs ` B ) ^ 2 ) )
17 13 16 eqtr3d 
 |-  ( B e. RR -> ( B ^ 2 ) = ( ( abs ` B ) ^ 2 ) )
18 9 17 eqeqan12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( ( abs ` A ) ^ 2 ) = ( ( abs ` B ) ^ 2 ) ) )
19 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
20 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
21 19 20 jca 
 |-  ( A e. CC -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
22 abscl 
 |-  ( B e. CC -> ( abs ` B ) e. RR )
23 absge0 
 |-  ( B e. CC -> 0 <_ ( abs ` B ) )
24 22 23 jca 
 |-  ( B e. CC -> ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) )
25 sq11 
 |-  ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) ) -> ( ( ( abs ` A ) ^ 2 ) = ( ( abs ` B ) ^ 2 ) <-> ( abs ` A ) = ( abs ` B ) ) )
26 21 24 25 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( abs ` A ) ^ 2 ) = ( ( abs ` B ) ^ 2 ) <-> ( abs ` A ) = ( abs ` B ) ) )
27 5 14 26 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( abs ` A ) ^ 2 ) = ( ( abs ` B ) ^ 2 ) <-> ( abs ` A ) = ( abs ` B ) ) )
28 18 27 bitrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( abs ` A ) = ( abs ` B ) ) )