mulgcddvds

Description: One half of rpmulgcd2 , which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015)

		Ref	Expression
	Assertion	mulgcddvds	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
2		simp2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \in ℤ$
3		simp3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to N \in ℤ$
4	2 3	zmulcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
5	1 4	gcdcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd M \cdot N \in ℕ_{0}$
6	5	nn0zd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd M \cdot N \in ℤ$
7		dvds0	$⊢ K \gcd M \cdot N \in ℤ \to (K \gcd M \cdot N) ∥ 0$
8	6 7	syl	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ 0$
9	8	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N = 0) \to (K \gcd M \cdot N) ∥ 0$
10		oveq2	$⊢ K \gcd N = 0 \to (K \gcd M) (K \gcd N) = (K \gcd M) \cdot 0$
11	1 2	gcdcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd M \in ℕ_{0}$
12	11	nn0cnd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd M \in ℂ$
13	12	mul01d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M) \cdot 0 = 0$
14	10 13	sylan9eqr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N = 0) \to (K \gcd M) (K \gcd N) = 0$
15	9 14	breqtrrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N = 0) \to (K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N)$
16	6	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to K \gcd M \cdot N \in ℤ$
17	16	zcnd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to K \gcd M \cdot N \in ℂ$
18	1 3	gcdcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd N \in ℕ_{0}$
19	18	nn0zd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd N \in ℤ$
20	19	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to K \gcd N \in ℤ$
21	20	zcnd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to K \gcd N \in ℂ$
22		simpr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to K \gcd N \neq 0$
23	17 21 22	divcan1d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) = K \gcd M \cdot N$
24		gcddvds	$⊢ (K \in ℤ \land M \cdot N \in ℤ) \to ((K \gcd M \cdot N) ∥ K \land (K \gcd M \cdot N) ∥ M \cdot N)$
25	1 4 24	syl2anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd M \cdot N) ∥ K \land (K \gcd M \cdot N) ∥ M \cdot N)$
26	25	simpld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ K$
27	6 1 19 26	dvdsmultr1d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ K (K \gcd N)$
28	27	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (K \gcd M \cdot N) ∥ K (K \gcd N)$
29	23 28	eqbrtrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ K (K \gcd N)$
30		gcddvds	$⊢ (K \in ℤ \land N \in ℤ) \to ((K \gcd N) ∥ K \land (K \gcd N) ∥ N)$
31	1 3 30	syl2anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd N) ∥ K \land (K \gcd N) ∥ N)$
32	31	simpld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd N) ∥ K$
33	31	simprd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd N) ∥ N$
34		dvdsmultr2	$⊢ (K \gcd N \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd N) ∥ N \to (K \gcd N) ∥ M \cdot N)$
35	19 2 3 34	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd N) ∥ N \to (K \gcd N) ∥ M \cdot N)$
36	33 35	mpd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd N) ∥ M \cdot N$
37		dvdsgcd	$⊢ (K \gcd N \in ℤ \land K \in ℤ \land M \cdot N \in ℤ) \to (((K \gcd N) ∥ K \land (K \gcd N) ∥ M \cdot N) \to (K \gcd N) ∥ (K \gcd M \cdot N))$
38	19 1 4 37	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (((K \gcd N) ∥ K \land (K \gcd N) ∥ M \cdot N) \to (K \gcd N) ∥ (K \gcd M \cdot N))$
39	32 36 38	mp2and	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd N) ∥ (K \gcd M \cdot N)$
40	39	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (K \gcd N) ∥ (K \gcd M \cdot N)$
41		dvdsval2	$⊢ (K \gcd N \in ℤ \land K \gcd N \neq 0 \land K \gcd M \cdot N \in ℤ) \to ((K \gcd N) ∥ (K \gcd M \cdot N) \leftrightarrow \frac{K \gcd M \cdot N}{K \gcd N} \in ℤ)$
42	20 22 16 41	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to ((K \gcd N) ∥ (K \gcd M \cdot N) \leftrightarrow \frac{K \gcd M \cdot N}{K \gcd N} \in ℤ)$
43	40 42	mpbid	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to \frac{K \gcd M \cdot N}{K \gcd N} \in ℤ$
44	1	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to K \in ℤ$
45		dvdsmulcr	$⊢ (\frac{K \gcd M \cdot N}{K \gcd N} \in ℤ \land K \in ℤ \land (K \gcd N \in ℤ \land K \gcd N \neq 0)) \to ((\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ K (K \gcd N) \leftrightarrow (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ K)$
46	43 44 20 22 45	syl112anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to ((\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ K (K \gcd N) \leftrightarrow (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ K)$
47	29 46	mpbid	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ K$
48		nn0abscl	$⊢ M \in ℤ \to \|M\| \in ℕ_{0}$
49	2 48	syl	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M\| \in ℕ_{0}$
50	49	nn0zd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M\| \in ℤ$
51		dvdsmultr2	$⊢ (K \gcd M \cdot N \in ℤ \land \|M\| \in ℤ \land K \in ℤ) \to ((K \gcd M \cdot N) ∥ K \to (K \gcd M \cdot N) ∥ \|M\| K)$
52	6 50 1 51	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd M \cdot N) ∥ K \to (K \gcd M \cdot N) ∥ \|M\| K)$
53	26 52	mpd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ \|M\| K$
54	50 3	zmulcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M\| \cdot N \in ℤ$
55	25	simprd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ M \cdot N$
56		iddvds	$⊢ M \in ℤ \to M ∥ M$
57	2 56	syl	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M ∥ M$
58		dvdsabsb	$⊢ (M \in ℤ \land M \in ℤ) \to (M ∥ M \leftrightarrow M ∥ \|M\|)$
59	2 2 58	syl2anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M ∥ M \leftrightarrow M ∥ \|M\|)$
60	57 59	mpbid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M ∥ \|M\|$
61		dvdsmulc	$⊢ (M \in ℤ \land \|M\| \in ℤ \land N \in ℤ) \to (M ∥ \|M\| \to M \cdot N ∥ \|M\| \cdot N)$
62	2 50 3 61	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M ∥ \|M\| \to M \cdot N ∥ \|M\| \cdot N)$
63	60 62	mpd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \cdot N ∥ \|M\| \cdot N$
64	6 4 54 55 63	dvdstrd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ \|M\| \cdot N$
65	50 1	zmulcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M\| K \in ℤ$
66		dvdsgcd	$⊢ (K \gcd M \cdot N \in ℤ \land \|M\| K \in ℤ \land \|M\| \cdot N \in ℤ) \to (((K \gcd M \cdot N) ∥ \|M\| K \land (K \gcd M \cdot N) ∥ \|M\| \cdot N) \to (K \gcd M \cdot N) ∥ (\|M\| K \gcd \|M\| \cdot N))$
67	6 65 54 66	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (((K \gcd M \cdot N) ∥ \|M\| K \land (K \gcd M \cdot N) ∥ \|M\| \cdot N) \to (K \gcd M \cdot N) ∥ (\|M\| K \gcd \|M\| \cdot N))$
68	53 64 67	mp2and	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ (\|M\| K \gcd \|M\| \cdot N)$
69	18	nn0red	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd N \in ℝ$
70	18	nn0ge0d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to 0 \leq K \gcd N$
71	69 70	absidd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|K \gcd N\| = K \gcd N$
72	71	oveq2d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M\| \|K \gcd N\| = \|M\| (K \gcd N)$
73	2	zcnd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \in ℂ$
74	18	nn0cnd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd N \in ℂ$
75	73 74	absmuld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M (K \gcd N)\| = \|M\| \|K \gcd N\|$
76		mulgcd	$⊢ (\|M\| \in ℕ_{0} \land K \in ℤ \land N \in ℤ) \to \|M\| K \gcd \|M\| \cdot N = \|M\| (K \gcd N)$
77	49 1 3 76	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M\| K \gcd \|M\| \cdot N = \|M\| (K \gcd N)$
78	72 75 77	3eqtr4d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M (K \gcd N)\| = \|M\| K \gcd \|M\| \cdot N$
79	68 78	breqtrrd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ \|M (K \gcd N)\|$
80	2 19	zmulcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M (K \gcd N) \in ℤ$
81		dvdsabsb	$⊢ (K \gcd M \cdot N \in ℤ \land M (K \gcd N) \in ℤ) \to ((K \gcd M \cdot N) ∥ M (K \gcd N) \leftrightarrow (K \gcd M \cdot N) ∥ \|M (K \gcd N)\|)$
82	6 80 81	syl2anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd M \cdot N) ∥ M (K \gcd N) \leftrightarrow (K \gcd M \cdot N) ∥ \|M (K \gcd N)\|)$
83	79 82	mpbird	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ M (K \gcd N)$
84	83	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (K \gcd M \cdot N) ∥ M (K \gcd N)$
85	23 84	eqbrtrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ M (K \gcd N)$
86	2	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to M \in ℤ$
87		dvdsmulcr	$⊢ (\frac{K \gcd M \cdot N}{K \gcd N} \in ℤ \land M \in ℤ \land (K \gcd N \in ℤ \land K \gcd N \neq 0)) \to ((\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ M (K \gcd N) \leftrightarrow (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ M)$
88	43 86 20 22 87	syl112anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to ((\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ M (K \gcd N) \leftrightarrow (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ M)$
89	85 88	mpbid	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ M$
90		dvdsgcd	$⊢ (\frac{K \gcd M \cdot N}{K \gcd N} \in ℤ \land K \in ℤ \land M \in ℤ) \to (((\frac{K \gcd M \cdot N}{K \gcd N}) ∥ K \land (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ M) \to (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ (K \gcd M))$
91	43 44 86 90	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (((\frac{K \gcd M \cdot N}{K \gcd N}) ∥ K \land (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ M) \to (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ (K \gcd M))$
92	47 89 91	mp2and	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (\frac{K \gcd M \cdot N}{K \gcd N}) ∥ (K \gcd M)$
93	11	nn0zd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd M \in ℤ$
94	93	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to K \gcd M \in ℤ$
95		dvdsmulc	$⊢ (\frac{K \gcd M \cdot N}{K \gcd N} \in ℤ \land K \gcd M \in ℤ \land K \gcd N \in ℤ) \to ((\frac{K \gcd M \cdot N}{K \gcd N}) ∥ (K \gcd M) \to (\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ (K \gcd M) (K \gcd N))$
96	43 94 20 95	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to ((\frac{K \gcd M \cdot N}{K \gcd N}) ∥ (K \gcd M) \to (\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ (K \gcd M) (K \gcd N))$
97	92 96	mpd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (\frac{K \gcd M \cdot N}{K \gcd N}) (K \gcd N) ∥ (K \gcd M) (K \gcd N)$
98	23 97	eqbrtrrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd N \neq 0) \to (K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N)$
99	15 98	pm2.61dane	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N)$

Metamath Proof Explorer

Theorem mulgcddvds

Proof