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 0 M N K M gcd K N = K M gcd N

Proof

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