# Metamath Proof Explorer

## Theorem rpmulgcd

Description: If K and M are relatively prime, then the GCD of K and M x. N is the GCD of K and N . (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion rpmulgcd
`|- ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( K gcd ( M x. N ) ) = ( K gcd N ) )`

### Proof

Step Hyp Ref Expression
1 gcdmultiple
` |-  ( ( K e. NN /\ N e. NN ) -> ( K gcd ( K x. N ) ) = K )`
2 1 3adant2
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( K gcd ( K x. N ) ) = K )`
3 2 oveq1d
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( ( K gcd ( K x. N ) ) gcd ( M x. N ) ) = ( K gcd ( M x. N ) ) )`
4 nnz
` |-  ( K e. NN -> K e. ZZ )`
5 4 3ad2ant1
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> K e. ZZ )`
6 nnz
` |-  ( N e. NN -> N e. ZZ )`
7 zmulcl
` |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K x. N ) e. ZZ )`
8 4 6 7 syl2an
` |-  ( ( K e. NN /\ N e. NN ) -> ( K x. N ) e. ZZ )`
9 8 3adant2
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( K x. N ) e. ZZ )`
10 nnz
` |-  ( M e. NN -> M e. ZZ )`
11 zmulcl
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )`
12 10 6 11 syl2an
` |-  ( ( M e. NN /\ N e. NN ) -> ( M x. N ) e. ZZ )`
13 12 3adant1
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( M x. N ) e. ZZ )`
14 gcdass
` |-  ( ( K e. ZZ /\ ( K x. N ) e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( K gcd ( K x. N ) ) gcd ( M x. N ) ) = ( K gcd ( ( K x. N ) gcd ( M x. N ) ) ) )`
15 5 9 13 14 syl3anc
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( ( K gcd ( K x. N ) ) gcd ( M x. N ) ) = ( K gcd ( ( K x. N ) gcd ( M x. N ) ) ) )`
16 3 15 eqtr3d
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( K gcd ( M x. N ) ) = ( K gcd ( ( K x. N ) gcd ( M x. N ) ) ) )`
17 16 adantr
` |-  ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( K gcd ( M x. N ) ) = ( K gcd ( ( K x. N ) gcd ( M x. N ) ) ) )`
18 nnnn0
` |-  ( N e. NN -> N e. NN0 )`
19 mulgcdr
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. NN0 ) -> ( ( K x. N ) gcd ( M x. N ) ) = ( ( K gcd M ) x. N ) )`
20 4 10 18 19 syl3an
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( ( K x. N ) gcd ( M x. N ) ) = ( ( K gcd M ) x. N ) )`
21 oveq1
` |-  ( ( K gcd M ) = 1 -> ( ( K gcd M ) x. N ) = ( 1 x. N ) )`
22 20 21 sylan9eq
` |-  ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( ( K x. N ) gcd ( M x. N ) ) = ( 1 x. N ) )`
23 nncn
` |-  ( N e. NN -> N e. CC )`
24 23 3ad2ant3
` |-  ( ( K e. NN /\ M e. NN /\ N e. NN ) -> N e. CC )`
25 24 adantr
` |-  ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> N e. CC )`
26 25 mulid2d
` |-  ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( 1 x. N ) = N )`
27 22 26 eqtrd
` |-  ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( ( K x. N ) gcd ( M x. N ) ) = N )`
28 27 oveq2d
` |-  ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( K gcd ( ( K x. N ) gcd ( M x. N ) ) ) = ( K gcd N ) )`
29 17 28 eqtrd
` |-  ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( K gcd ( M x. N ) ) = ( K gcd N ) )`