Metamath Proof Explorer

Theorem gcdabsorb

Description: Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 gcdass 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) gcd B ) = ( A gcd ( B gcd B ) ) )
2 1 3anidm23 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) gcd B ) = ( A gcd ( B gcd B ) ) )
3 gcdid 
 |-  ( B e. ZZ -> ( B gcd B ) = ( abs ` B ) )
4 3 oveq2d 
 |-  ( B e. ZZ -> ( A gcd ( B gcd B ) ) = ( A gcd ( abs ` B ) ) )
5 4 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd ( B gcd B ) ) = ( A gcd ( abs ` B ) ) )
6 gcdabs2 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd ( abs ` B ) ) = ( A gcd B ) )
7 2 5 6 3eqtrd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) gcd B ) = ( A gcd B ) )