This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
11 10 3adant1 
 |-  ( ( 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 ) )
49 48 3adant1 
 |-  ( ( 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
66 10 3adant1 
 |-  ( ( 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 )
73 72 3ad2ant2 
 |-  ( ( 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 )
78 77 3ad2ant3 
 |-  ( ( 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 ) ) )