# Metamath Proof Explorer

## Theorem mulgcdr

Description: Reverse distribution law for the gcd operator. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion mulgcdr
`|- ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( A x. C ) gcd ( B x. C ) ) = ( ( A gcd B ) x. C ) )`

### Proof

Step Hyp Ref Expression
1 mulgcd
` |-  ( ( C e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( C x. A ) gcd ( C x. B ) ) = ( C x. ( A gcd B ) ) )`
2 1 3coml
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( C x. A ) gcd ( C x. B ) ) = ( C x. ( A gcd B ) ) )`
3 zcn
` |-  ( A e. ZZ -> A e. CC )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> A e. CC )`
5 nn0cn
` |-  ( C e. NN0 -> C e. CC )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> C e. CC )`
7 4 6 mulcomd
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( A x. C ) = ( C x. A ) )`
8 zcn
` |-  ( B e. ZZ -> B e. CC )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> B e. CC )`
10 9 6 mulcomd
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( B x. C ) = ( C x. B ) )`
11 7 10 oveq12d
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( A x. C ) gcd ( B x. C ) ) = ( ( C x. A ) gcd ( C x. B ) ) )`
12 gcdcl
` |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( A gcd B ) e. NN0 )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( A gcd B ) e. CC )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( A gcd B ) x. C ) = ( C x. ( A gcd B ) ) )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( A x. C ) gcd ( B x. C ) ) = ( ( A gcd B ) x. C ) )`