This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpmul

Description: If K is relatively prime to M and to N , it is also relatively prime to their product. (Contributed by Mario Carneiro, 24-Feb-2014) (Proof shortened by Mario Carneiro, 2-Jul-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mulgcddvds	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N)$
2		oveq12	$⊢ (K \gcd M = 1 \land K \gcd N = 1) \to (K \gcd M) (K \gcd N) = 1 \cdot 1$
3		1t1e1	$⊢ 1 \cdot 1 = 1$
4	2 3	eqtrdi	$⊢ (K \gcd M = 1 \land K \gcd N = 1) \to (K \gcd M) (K \gcd N) = 1$
5	4	breq2d	$⊢ (K \gcd M = 1 \land K \gcd N = 1) \to ((K \gcd M \cdot N) ∥ (K \gcd M) (K \gcd N) \leftrightarrow (K \gcd M \cdot N) ∥ 1)$
6	1 5	syl5ibcom	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd M = 1 \land K \gcd N = 1) \to (K \gcd M \cdot N) ∥ 1)$
7		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
8		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
9	8	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
10	7 9	gcdcld	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd M \cdot N \in ℕ_{0}$
11		dvds1	$⊢ K \gcd M \cdot N \in ℕ_{0} \to ((K \gcd M \cdot N) ∥ 1 \leftrightarrow K \gcd M \cdot N = 1)$
12	10 11	syl	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd M \cdot N) ∥ 1 \leftrightarrow K \gcd M \cdot N = 1)$
13	6 12	sylibd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K \gcd M = 1 \land K \gcd N = 1) \to K \gcd M \cdot N = 1)$