Metamath Proof Explorer

Theorem rpmulgcd2

Description: If M is relatively prime to N , then the GCD of K with M x. N is the product of the GCDs with M and N respectively. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion rpmulgcd2 
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd ( M x. N ) ) = ( ( K gcd M ) x. ( K gcd N ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> K e. ZZ )
2 simpl2 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> M e. ZZ )
3 simpl3 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> N e. ZZ )
4 2 3 zmulcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( M x. N ) e. ZZ )
5 1 4 gcdcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd ( M x. N ) ) e. NN0 )
6 1 2 gcdcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd M ) e. NN0 )
7 1 3 gcdcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd N ) e. NN0 )
8 6 7 nn0mulcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) x. ( K gcd N ) ) e. NN0 )
9 mulgcddvds 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )
10 9 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )
11 gcddvds 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( ( K gcd M ) || K /\ ( K gcd M ) || M ) )
12 1 2 11 syl2anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) || K /\ ( K gcd M ) || M ) )
13 12 simpld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd M ) || K )
14 gcddvds 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( ( K gcd N ) || K /\ ( K gcd N ) || N ) )
15 1 3 14 syl2anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd N ) || K /\ ( K gcd N ) || N ) )
16 15 simpld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd N ) || K )
17 6 nn0zd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd M ) e. ZZ )
18 7 nn0zd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd N ) e. ZZ )
19 17 18 gcdcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) e. NN0 )
20 19 nn0zd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) e. ZZ )
21 gcddvds 
 |-  ( ( ( K gcd M ) e. ZZ /\ ( K gcd N ) e. ZZ ) -> ( ( ( K gcd M ) gcd ( K gcd N ) ) || ( K gcd M ) /\ ( ( K gcd M ) gcd ( K gcd N ) ) || ( K gcd N ) ) )
22 17 18 21 syl2anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( ( K gcd M ) gcd ( K gcd N ) ) || ( K gcd M ) /\ ( ( K gcd M ) gcd ( K gcd N ) ) || ( K gcd N ) ) )
23 22 simpld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || ( K gcd M ) )
24 12 simprd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd M ) || M )
25 20 17 2 23 24 dvdstrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || M )
26 22 simprd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || ( K gcd N ) )
27 15 simprd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd N ) || N )
28 20 18 3 26 27 dvdstrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || N )
29 dvdsgcd 
 |-  ( ( ( ( K gcd M ) gcd ( K gcd N ) ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( ( K gcd M ) gcd ( K gcd N ) ) || M /\ ( ( K gcd M ) gcd ( K gcd N ) ) || N ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || ( M gcd N ) ) )
30 20 2 3 29 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( ( ( K gcd M ) gcd ( K gcd N ) ) || M /\ ( ( K gcd M ) gcd ( K gcd N ) ) || N ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || ( M gcd N ) ) )
31 25 28 30 mp2and 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || ( M gcd N ) )
32 simpr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( M gcd N ) = 1 )
33 31 32 breqtrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) || 1 )
34 dvds1 
 |-  ( ( ( K gcd M ) gcd ( K gcd N ) ) e. NN0 -> ( ( ( K gcd M ) gcd ( K gcd N ) ) || 1 <-> ( ( K gcd M ) gcd ( K gcd N ) ) = 1 ) )
35 19 34 syl 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( ( K gcd M ) gcd ( K gcd N ) ) || 1 <-> ( ( K gcd M ) gcd ( K gcd N ) ) = 1 ) )
36 33 35 mpbid 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) gcd ( K gcd N ) ) = 1 )
37 coprmdvds2 
 |-  ( ( ( ( K gcd M ) e. ZZ /\ ( K gcd N ) e. ZZ /\ K e. ZZ ) /\ ( ( K gcd M ) gcd ( K gcd N ) ) = 1 ) -> ( ( ( K gcd M ) || K /\ ( K gcd N ) || K ) -> ( ( K gcd M ) x. ( K gcd N ) ) || K ) )
38 17 18 1 36 37 syl31anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( ( K gcd M ) || K /\ ( K gcd N ) || K ) -> ( ( K gcd M ) x. ( K gcd N ) ) || K ) )
39 13 16 38 mp2and 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) x. ( K gcd N ) ) || K )
40 dvdscmul 
 |-  ( ( ( K gcd N ) e. ZZ /\ N e. ZZ /\ ( K gcd M ) e. ZZ ) -> ( ( K gcd N ) || N -> ( ( K gcd M ) x. ( K gcd N ) ) || ( ( K gcd M ) x. N ) ) )
41 18 3 17 40 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd N ) || N -> ( ( K gcd M ) x. ( K gcd N ) ) || ( ( K gcd M ) x. N ) ) )
42 dvdsmulc 
 |-  ( ( ( K gcd M ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd M ) || M -> ( ( K gcd M ) x. N ) || ( M x. N ) ) )
43 17 2 3 42 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) || M -> ( ( K gcd M ) x. N ) || ( M x. N ) ) )
44 17 18 zmulcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) x. ( K gcd N ) ) e. ZZ )
45 17 3 zmulcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) x. N ) e. ZZ )
46 dvdstr 
 |-  ( ( ( ( K gcd M ) x. ( K gcd N ) ) e. ZZ /\ ( ( K gcd M ) x. N ) e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( ( ( K gcd M ) x. ( K gcd N ) ) || ( ( K gcd M ) x. N ) /\ ( ( K gcd M ) x. N ) || ( M x. N ) ) -> ( ( K gcd M ) x. ( K gcd N ) ) || ( M x. N ) ) )
47 44 45 4 46 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( ( ( K gcd M ) x. ( K gcd N ) ) || ( ( K gcd M ) x. N ) /\ ( ( K gcd M ) x. N ) || ( M x. N ) ) -> ( ( K gcd M ) x. ( K gcd N ) ) || ( M x. N ) ) )
48 41 43 47 syl2and 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( ( K gcd N ) || N /\ ( K gcd M ) || M ) -> ( ( K gcd M ) x. ( K gcd N ) ) || ( M x. N ) ) )
49 27 24 48 mp2and 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) x. ( K gcd N ) ) || ( M x. N ) )
50 dvdsgcd 
 |-  ( ( ( ( K gcd M ) x. ( K gcd N ) ) e. ZZ /\ K e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( ( ( K gcd M ) x. ( K gcd N ) ) || K /\ ( ( K gcd M ) x. ( K gcd N ) ) || ( M x. N ) ) -> ( ( K gcd M ) x. ( K gcd N ) ) || ( K gcd ( M x. N ) ) ) )
51 44 1 4 50 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( ( ( K gcd M ) x. ( K gcd N ) ) || K /\ ( ( K gcd M ) x. ( K gcd N ) ) || ( M x. N ) ) -> ( ( K gcd M ) x. ( K gcd N ) ) || ( K gcd ( M x. N ) ) ) )
52 39 49 51 mp2and 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( K gcd M ) x. ( K gcd N ) ) || ( K gcd ( M x. N ) ) )
53 dvdseq 
 |-  ( ( ( ( K gcd ( M x. N ) ) e. NN0 /\ ( ( K gcd M ) x. ( K gcd N ) ) e. NN0 ) /\ ( ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) /\ ( ( K gcd M ) x. ( K gcd N ) ) || ( K gcd ( M x. N ) ) ) ) -> ( K gcd ( M x. N ) ) = ( ( K gcd M ) x. ( K gcd N ) ) )
54 5 8 10 52 53 syl22anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( K gcd ( M x. N ) ) = ( ( K gcd M ) x. ( K gcd N ) ) )