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 \in ℕ_{0} \land M \in ℤ \land N \in ℤ) \to K \cdot M \gcd K \cdot N = K (M \gcd N)$

Proof

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

Metamath Proof Explorer

Theorem mulgcd

Proof