Metamath Proof Explorer

Theorem zgcdsq

Description: nn0gcdsq extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion zgcdsq 
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 gcdabs 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( abs ` A ) gcd ( abs ` B ) ) = ( A gcd B ) )
2 1 eqcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( ( abs ` A ) gcd ( abs ` B ) ) )
3 2 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) ^ 2 ) = ( ( ( abs ` A ) gcd ( abs ` B ) ) ^ 2 ) )
4 nn0abscl 
 |-  ( A e. ZZ -> ( abs ` A ) e. NN0 )
5 nn0abscl 
 |-  ( B e. ZZ -> ( abs ` B ) e. NN0 )
6 nn0gcdsq 
 |-  ( ( ( abs ` A ) e. NN0 /\ ( abs ` B ) e. NN0 ) -> ( ( ( abs ` A ) gcd ( abs ` B ) ) ^ 2 ) = ( ( ( abs ` A ) ^ 2 ) gcd ( ( abs ` B ) ^ 2 ) ) )
7 4 5 6 syl2an 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( abs ` A ) gcd ( abs ` B ) ) ^ 2 ) = ( ( ( abs ` A ) ^ 2 ) gcd ( ( abs ` B ) ^ 2 ) ) )
8 zre 
 |-  ( A e. ZZ -> A e. RR )
9 8 adantr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. RR )
10 absresq 
 |-  ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
11 9 10 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
12 zre 
 |-  ( B e. ZZ -> B e. RR )
13 12 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. RR )
14 absresq 
 |-  ( B e. RR -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) )
15 13 14 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) )
16 11 15 oveq12d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( abs ` A ) ^ 2 ) gcd ( ( abs ` B ) ^ 2 ) ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
17 3 7 16 3eqtrd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )