rpmulgcd

Description: If K and M are relatively prime, then the gcd of K and M x. N is the gcd of K and N . (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		gcdmultiple	$⊢ (K \in ℕ \land N \in ℕ) \to K \gcd K \cdot N = K$
2	1	3adant2	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to K \gcd K \cdot N = K$
3	2	oveq1d	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to (K \gcd K \cdot N) \gcd M \cdot N = K \gcd M \cdot N$
4		nnz	$⊢ K \in ℕ \to K \in ℤ$
5	4	3ad2ant1	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to K \in ℤ$
6		nnz	$⊢ N \in ℕ \to N \in ℤ$
7		zmulcl	$⊢ (K \in ℤ \land N \in ℤ) \to K \cdot N \in ℤ$
8	4 6 7	syl2an	$⊢ (K \in ℕ \land N \in ℕ) \to K \cdot N \in ℤ$
9	8	3adant2	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to K \cdot N \in ℤ$
10		nnz	$⊢ M \in ℕ \to M \in ℤ$
11		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
12	10 6 11	syl2an	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N \in ℤ$
13	12	3adant1	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to M \cdot N \in ℤ$
14		gcdass	$⊢ (K \in ℤ \land K \cdot N \in ℤ \land M \cdot N \in ℤ) \to (K \gcd K \cdot N) \gcd M \cdot N = K \gcd (K \cdot N \gcd M \cdot N)$
15	5 9 13 14	syl3anc	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to (K \gcd K \cdot N) \gcd M \cdot N = K \gcd (K \cdot N \gcd M \cdot N)$
16	3 15	eqtr3d	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to K \gcd M \cdot N = K \gcd (K \cdot N \gcd M \cdot N)$
17	16	adantr	$⊢ ((K \in ℕ \land M \in ℕ \land N \in ℕ) \land K \gcd M = 1) \to K \gcd M \cdot N = K \gcd (K \cdot N \gcd M \cdot N)$
18		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
19		mulgcdr	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℕ_{0}) \to K \cdot N \gcd M \cdot N = (K \gcd M) \cdot N$
20	4 10 18 19	syl3an	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to K \cdot N \gcd M \cdot N = (K \gcd M) \cdot N$
21		oveq1	$⊢ K \gcd M = 1 \to (K \gcd M) \cdot N = 1 \cdot N$
22	20 21	sylan9eq	$⊢ ((K \in ℕ \land M \in ℕ \land N \in ℕ) \land K \gcd M = 1) \to K \cdot N \gcd M \cdot N = 1 \cdot N$
23		nncn	$⊢ N \in ℕ \to N \in ℂ$
24	23	3ad2ant3	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to N \in ℂ$
25	24	adantr	$⊢ ((K \in ℕ \land M \in ℕ \land N \in ℕ) \land K \gcd M = 1) \to N \in ℂ$
26	25	mullidd	$⊢ ((K \in ℕ \land M \in ℕ \land N \in ℕ) \land K \gcd M = 1) \to 1 \cdot N = N$
27	22 26	eqtrd	$⊢ ((K \in ℕ \land M \in ℕ \land N \in ℕ) \land K \gcd M = 1) \to K \cdot N \gcd M \cdot N = N$
28	27	oveq2d	$⊢ ((K \in ℕ \land M \in ℕ \land N \in ℕ) \land K \gcd M = 1) \to K \gcd (K \cdot N \gcd M \cdot N) = K \gcd N$
29	17 28	eqtrd	$⊢ ((K \in ℕ \land M \in ℕ \land N \in ℕ) \land K \gcd M = 1) \to K \gcd M \cdot N = K \gcd N$

Metamath Proof Explorer

Theorem rpmulgcd

Proof