rpmulgcd2

Description: If M is relatively prime to N , then the GCD of K with M x. N is the product of the GCDs with M and N respectively. (Contributed by Mario Carneiro, 2-Jul-2015)

		Ref	Expression
	Assertion	rpmulgcd2	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \gcd M \cdot N = (K \gcd M) (K \gcd N)$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \in ℤ$
2		simpl2	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to M \in ℤ$
3		simpl3	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to N \in ℤ$
4	2 3	zmulcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to M \cdot N \in ℤ$
5	1 4	gcdcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \gcd M \cdot N \in ℕ_{0}$
6	1 2	gcdcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \gcd M \in ℕ_{0}$
7	1 3	gcdcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \gcd N \in ℕ_{0}$
8	6 7	nn0mulcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) (K \gcd N) \in ℕ_{0}$
9		mulgcddvds	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N)$
10	9	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N)$
11		gcddvds	$⊢ (K \in ℤ \land M \in ℤ) \to ((K \gcd M) ∥ K \land (K \gcd M) ∥ M)$
12	1 2 11	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) ∥ K \land (K \gcd M) ∥ M)$
13	12	simpld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) ∥ K$
14		gcddvds	$⊢ (K \in ℤ \land N \in ℤ) \to ((K \gcd N) ∥ K \land (K \gcd N) ∥ N)$
15	1 3 14	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd N) ∥ K \land (K \gcd N) ∥ N)$
16	15	simpld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd N) ∥ K$
17	6	nn0zd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \gcd M \in ℤ$
18	7	nn0zd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \gcd N \in ℤ$
19	17 18	gcdcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) \gcd (K \gcd N) \in ℕ_{0}$
20	19	nn0zd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) \gcd (K \gcd N) \in ℤ$
21		gcddvds	$⊢ (K \gcd M \in ℤ \land K \gcd N \in ℤ) \to (((K \gcd M) \gcd (K \gcd N)) ∥ (K \gcd M) \land ((K \gcd M) \gcd (K \gcd N)) ∥ (K \gcd N))$
22	17 18 21	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (((K \gcd M) \gcd (K \gcd N)) ∥ (K \gcd M) \land ((K \gcd M) \gcd (K \gcd N)) ∥ (K \gcd N))$
23	22	simpld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) \gcd (K \gcd N)) ∥ (K \gcd M)$
24	12	simprd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) ∥ M$
25	20 17 2 23 24	dvdstrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) \gcd (K \gcd N)) ∥ M$
26	22	simprd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) \gcd (K \gcd N)) ∥ (K \gcd N)$
27	15	simprd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd N) ∥ N$
28	20 18 3 26 27	dvdstrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) \gcd (K \gcd N)) ∥ N$
29		dvdsgcd	$⊢ ((K \gcd M) \gcd (K \gcd N) \in ℤ \land M \in ℤ \land N \in ℤ) \to ((((K \gcd M) \gcd (K \gcd N)) ∥ M \land ((K \gcd M) \gcd (K \gcd N)) ∥ N) \to ((K \gcd M) \gcd (K \gcd N)) ∥ (M \gcd N))$
30	20 2 3 29	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((((K \gcd M) \gcd (K \gcd N)) ∥ M \land ((K \gcd M) \gcd (K \gcd N)) ∥ N) \to ((K \gcd M) \gcd (K \gcd N)) ∥ (M \gcd N))$
31	25 28 30	mp2and	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) \gcd (K \gcd N)) ∥ (M \gcd N)$
32		simpr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to M \gcd N = 1$
33	31 32	breqtrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) \gcd (K \gcd N)) ∥ 1$
34		dvds1	$⊢ (K \gcd M) \gcd (K \gcd N) \in ℕ_{0} \to (((K \gcd M) \gcd (K \gcd N)) ∥ 1 \leftrightarrow (K \gcd M) \gcd (K \gcd N) = 1)$
35	19 34	syl	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (((K \gcd M) \gcd (K \gcd N)) ∥ 1 \leftrightarrow (K \gcd M) \gcd (K \gcd N) = 1)$
36	33 35	mpbid	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) \gcd (K \gcd N) = 1$
37		coprmdvds2	$⊢ ((K \gcd M \in ℤ \land K \gcd N \in ℤ \land K \in ℤ) \land (K \gcd M) \gcd (K \gcd N) = 1) \to (((K \gcd M) ∥ K \land (K \gcd N) ∥ K) \to (K \gcd M) (K \gcd N) ∥ K)$
38	17 18 1 36 37	syl31anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (((K \gcd M) ∥ K \land (K \gcd N) ∥ K) \to (K \gcd M) (K \gcd N) ∥ K)$
39	13 16 38	mp2and	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) (K \gcd N) ∥ K$
40		dvdscmul	$⊢ (K \gcd N \in ℤ \land N \in ℤ \land K \gcd M \in ℤ) \to ((K \gcd N) ∥ N \to (K \gcd M) (K \gcd N) ∥ (K \gcd M) \cdot N)$
41	18 3 17 40	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd N) ∥ N \to (K \gcd M) (K \gcd N) ∥ (K \gcd M) \cdot N)$
42		dvdsmulc	$⊢ (K \gcd M \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd M) ∥ M \to (K \gcd M) \cdot N ∥ M \cdot N)$
43	17 2 3 42	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to ((K \gcd M) ∥ M \to (K \gcd M) \cdot N ∥ M \cdot N)$
44	17 18	zmulcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) (K \gcd N) \in ℤ$
45	17 3	zmulcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) \cdot N \in ℤ$
46		dvdstr	$⊢ ((K \gcd M) (K \gcd N) \in ℤ \land (K \gcd M) \cdot N \in ℤ \land M \cdot N \in ℤ) \to (((K \gcd M) (K \gcd N) ∥ (K \gcd M) \cdot N \land (K \gcd M) \cdot N ∥ M \cdot N) \to (K \gcd M) (K \gcd N) ∥ M \cdot N)$
47	44 45 4 46	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (((K \gcd M) (K \gcd N) ∥ (K \gcd M) \cdot N \land (K \gcd M) \cdot N ∥ M \cdot N) \to (K \gcd M) (K \gcd N) ∥ M \cdot N)$
48	41 43 47	syl2and	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (((K \gcd N) ∥ N \land (K \gcd M) ∥ M) \to (K \gcd M) (K \gcd N) ∥ M \cdot N)$
49	27 24 48	mp2and	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) (K \gcd N) ∥ M \cdot N$
50		dvdsgcd	$⊢ ((K \gcd M) (K \gcd N) \in ℤ \land K \in ℤ \land M \cdot N \in ℤ) \to (((K \gcd M) (K \gcd N) ∥ K \land (K \gcd M) (K \gcd N) ∥ M \cdot N) \to (K \gcd M) (K \gcd N) ∥ (K \gcd M \cdot N))$
51	44 1 4 50	syl3anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (((K \gcd M) (K \gcd N) ∥ K \land (K \gcd M) (K \gcd N) ∥ M \cdot N) \to (K \gcd M) (K \gcd N) ∥ (K \gcd M \cdot N))$
52	39 49 51	mp2and	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to (K \gcd M) (K \gcd N) ∥ (K \gcd M \cdot N)$
53		dvdseq	$⊢ ((K \gcd M \cdot N \in ℕ_{0} \land (K \gcd M) (K \gcd N) \in ℕ_{0}) \land ((K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N) \land (K \gcd M) (K \gcd N) ∥ (K \gcd M \cdot N))) \to K \gcd M \cdot N = (K \gcd M) (K \gcd N)$
54	5 8 10 52 53	syl22anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to K \gcd M \cdot N = (K \gcd M) (K \gcd N)$

Metamath Proof Explorer

Theorem rpmulgcd2

Proof