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 )
4 3 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> A e. CC )
5 nn0cn 
 |-  ( C e. NN0 -> C e. CC )
6 5 3ad2ant3 
 |-  ( ( 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 )
9 8 3ad2ant2 
 |-  ( ( 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 )
13 12 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( A gcd B ) e. NN0 )
14 13 nn0cnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( A gcd B ) e. CC )
15 14 6 mulcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( A gcd B ) x. C ) = ( C x. ( A gcd B ) ) )
16 2 11 15 3eqtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( A x. C ) gcd ( B x. C ) ) = ( ( A gcd B ) x. C ) )