# Metamath Proof Explorer

## Theorem mulgcd

Description: Distribute multiplication by a nonnegative integer over gcd. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Mario Carneiro, 30-May-2014)

Ref Expression
Assertion mulgcd
`|- ( ( K e. NN0 /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) )`

### Proof

Step Hyp Ref Expression
1 elnn0
` |-  ( K e. NN0 <-> ( K e. NN \/ K = 0 ) )`
2 simp1
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K e. NN )`
3 2 nnzd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )`
4 simp2
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> M e. ZZ )`
5 3 4 zmulcld
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. M ) e. ZZ )`
6 simp3
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> N e. ZZ )`
7 3 6 zmulcld
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. N ) e. ZZ )`
8 5 7 gcdcld
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) e. NN0 )`
9 2 nnnn0d
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K e. NN0 )`
10 gcdcl
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )`
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )`
12 9 11 nn0mulcld
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( M gcd N ) ) e. NN0 )`
13 8 nn0cnd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) e. CC )`
14 2 nncnd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K e. CC )`
15 2 nnne0d
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K =/= 0 )`
16 13 14 15 divcan2d
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) = ( ( K x. M ) gcd ( K x. N ) ) )`
17 gcddvds
` |-  ( ( ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ ) -> ( ( ( K x. M ) gcd ( K x. N ) ) || ( K x. M ) /\ ( ( K x. M ) gcd ( K x. N ) ) || ( K x. N ) ) )`
18 5 7 17 syl2anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K x. M ) gcd ( K x. N ) ) || ( K x. M ) /\ ( ( K x. M ) gcd ( K x. N ) ) || ( K x. N ) ) )`
19 18 simpld
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) || ( K x. M ) )`
20 16 19 eqbrtrd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. M ) )`
21 dvdsmul1
` |-  ( ( K e. ZZ /\ M e. ZZ ) -> K || ( K x. M ) )`
22 3 4 21 syl2anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K || ( K x. M ) )`
23 dvdsmul1
` |-  ( ( K e. ZZ /\ N e. ZZ ) -> K || ( K x. N ) )`
24 3 6 23 syl2anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K || ( K x. N ) )`
25 dvdsgcd
` |-  ( ( K e. ZZ /\ ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ ) -> ( ( K || ( K x. M ) /\ K || ( K x. N ) ) -> K || ( ( K x. M ) gcd ( K x. N ) ) ) )`
26 3 5 7 25 syl3anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( K x. M ) /\ K || ( K x. N ) ) -> K || ( ( K x. M ) gcd ( K x. N ) ) ) )`
27 22 24 26 mp2and
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> K || ( ( K x. M ) gcd ( K x. N ) ) )`
28 8 nn0zd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) e. ZZ )`
29 dvdsval2
` |-  ( ( K e. ZZ /\ K =/= 0 /\ ( ( K x. M ) gcd ( K x. N ) ) e. ZZ ) -> ( K || ( ( K x. M ) gcd ( K x. N ) ) <-> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) e. ZZ ) )`
30 3 15 28 29 syl3anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K || ( ( K x. M ) gcd ( K x. N ) ) <-> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) e. ZZ ) )`
31 27 30 mpbid
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) e. ZZ )`
32 dvdscmulr
` |-  ( ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) e. ZZ /\ M e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. M ) <-> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || M ) )`
33 31 4 3 15 32 syl112anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. M ) <-> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || M ) )`
34 20 33 mpbid
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || M )`
35 18 simprd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) || ( K x. N ) )`
36 16 35 eqbrtrd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. N ) )`
37 dvdscmulr
` |-  ( ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. N ) <-> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || N ) )`
38 31 6 3 15 37 syl112anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. N ) <-> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || N ) )`
39 36 38 mpbid
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || N )`
40 dvdsgcd
` |-  ( ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || M /\ ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || N ) -> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || ( M gcd N ) ) )`
41 31 4 6 40 syl3anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || M /\ ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || N ) -> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || ( M gcd N ) ) )`
42 34 39 41 mp2and
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || ( M gcd N ) )`
43 11 nn0zd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. ZZ )`
44 dvdscmul
` |-  ( ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) e. ZZ /\ ( M gcd N ) e. ZZ /\ K e. ZZ ) -> ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || ( M gcd N ) -> ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. ( M gcd N ) ) ) )`
45 31 43 3 44 syl3anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( ( K x. M ) gcd ( K x. N ) ) / K ) || ( M gcd N ) -> ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. ( M gcd N ) ) ) )`
46 42 45 mpd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( ( ( K x. M ) gcd ( K x. N ) ) / K ) ) || ( K x. ( M gcd N ) ) )`
47 16 46 eqbrtrrd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) || ( K x. ( M gcd N ) ) )`
48 gcddvds
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )`
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )`
50 49 simpld
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || M )`
51 dvdscmul
` |-  ( ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ K e. ZZ ) -> ( ( M gcd N ) || M -> ( K x. ( M gcd N ) ) || ( K x. M ) ) )`
52 43 4 3 51 syl3anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M -> ( K x. ( M gcd N ) ) || ( K x. M ) ) )`
53 50 52 mpd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( M gcd N ) ) || ( K x. M ) )`
54 49 simprd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || N )`
55 dvdscmul
` |-  ( ( ( M gcd N ) e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( M gcd N ) || N -> ( K x. ( M gcd N ) ) || ( K x. N ) ) )`
56 43 6 3 55 syl3anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || N -> ( K x. ( M gcd N ) ) || ( K x. N ) ) )`
57 54 56 mpd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( M gcd N ) ) || ( K x. N ) )`
58 12 nn0zd
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( M gcd N ) ) e. ZZ )`
59 dvdsgcd
` |-  ( ( ( K x. ( M gcd N ) ) e. ZZ /\ ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ ) -> ( ( ( K x. ( M gcd N ) ) || ( K x. M ) /\ ( K x. ( M gcd N ) ) || ( K x. N ) ) -> ( K x. ( M gcd N ) ) || ( ( K x. M ) gcd ( K x. N ) ) ) )`
60 58 5 7 59 syl3anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K x. ( M gcd N ) ) || ( K x. M ) /\ ( K x. ( M gcd N ) ) || ( K x. N ) ) -> ( K x. ( M gcd N ) ) || ( ( K x. M ) gcd ( K x. N ) ) ) )`
61 53 57 60 mp2and
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( M gcd N ) ) || ( ( K x. M ) gcd ( K x. N ) ) )`
62 dvdseq
` |-  ( ( ( ( ( K x. M ) gcd ( K x. N ) ) e. NN0 /\ ( K x. ( M gcd N ) ) e. NN0 ) /\ ( ( ( K x. M ) gcd ( K x. N ) ) || ( K x. ( M gcd N ) ) /\ ( K x. ( M gcd N ) ) || ( ( K x. M ) gcd ( K x. N ) ) ) ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) )`
63 8 12 47 61 62 syl22anc
` |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) )`
64 63 3expib
` |-  ( K e. NN -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) ) )`
65 gcd0val
` |-  ( 0 gcd 0 ) = 0`
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )`
67 66 nn0cnd
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. CC )`
68 67 mul02d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( 0 x. ( M gcd N ) ) = 0 )`
69 65 68 eqtr4id
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( 0 gcd 0 ) = ( 0 x. ( M gcd N ) ) )`
70 simp1
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> K = 0 )`
71 70 oveq1d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( K x. M ) = ( 0 x. M ) )`
72 zcn
` |-  ( M e. ZZ -> M e. CC )`
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> M e. CC )`
74 73 mul02d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( 0 x. M ) = 0 )`
75 71 74 eqtrd
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( K x. M ) = 0 )`
76 70 oveq1d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( K x. N ) = ( 0 x. N ) )`
77 zcn
` |-  ( N e. ZZ -> N e. CC )`
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> N e. CC )`
79 78 mul02d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( 0 x. N ) = 0 )`
80 76 79 eqtrd
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( K x. N ) = 0 )`
81 75 80 oveq12d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( 0 gcd 0 ) )`
82 70 oveq1d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( K x. ( M gcd N ) ) = ( 0 x. ( M gcd N ) ) )`
83 69 81 82 3eqtr4d
` |-  ( ( K = 0 /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) )`
84 83 3expib
` |-  ( K = 0 -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) ) )`
85 64 84 jaoi
` |-  ( ( K e. NN \/ K = 0 ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) ) )`
86 1 85 sylbi
` |-  ( K e. NN0 -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) ) )`
87 86 3impib
` |-  ( ( K e. NN0 /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) )`