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 ) )