coprmdvds2

Description: If an integer is divisible by two coprime integers, then it is divisible by their product. (Contributed by Mario Carneiro, 24-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		divides	$⊢ (N \in ℤ \land K \in ℤ) \to (N ∥ K \leftrightarrow \exists x \in ℤ x \cdot N = K)$
2	1	3adant1	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (N ∥ K \leftrightarrow \exists x \in ℤ x \cdot N = K)$
3	2	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \gcd N = 1) \to (N ∥ K \leftrightarrow \exists x \in ℤ x \cdot N = K)$
4		simprr	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to x \in ℤ$
5		simpl2	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to N \in ℤ$
6		zcn	$⊢ x \in ℤ \to x \in ℂ$
7		zcn	$⊢ N \in ℤ \to N \in ℂ$
8		mulcom	$⊢ (x \in ℂ \land N \in ℂ) \to x \cdot N = N x$
9	6 7 8	syl2an	$⊢ (x \in ℤ \land N \in ℤ) \to x \cdot N = N x$
10	4 5 9	syl2anc	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to x \cdot N = N x$
11	10	breq2d	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to (M ∥ x \cdot N \leftrightarrow M ∥ N x)$
12		simprl	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to M \gcd N = 1$
13		simpl1	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to M \in ℤ$
14		coprmdvds	$⊢ (M \in ℤ \land N \in ℤ \land x \in ℤ) \to ((M ∥ N x \land M \gcd N = 1) \to M ∥ x)$
15	13 5 4 14	syl3anc	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to ((M ∥ N x \land M \gcd N = 1) \to M ∥ x)$
16	12 15	mpan2d	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to (M ∥ N x \to M ∥ x)$
17	11 16	sylbid	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to (M ∥ x \cdot N \to M ∥ x)$
18		dvdsmulc	$⊢ (M \in ℤ \land x \in ℤ \land N \in ℤ) \to (M ∥ x \to M \cdot N ∥ x \cdot N)$
19	13 4 5 18	syl3anc	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to (M ∥ x \to M \cdot N ∥ x \cdot N)$
20	17 19	syld	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to (M ∥ x \cdot N \to M \cdot N ∥ x \cdot N)$
21		breq2	$⊢ x \cdot N = K \to (M ∥ x \cdot N \leftrightarrow M ∥ K)$
22		breq2	$⊢ x \cdot N = K \to (M \cdot N ∥ x \cdot N \leftrightarrow M \cdot N ∥ K)$
23	21 22	imbi12d	$⊢ x \cdot N = K \to ((M ∥ x \cdot N \to M \cdot N ∥ x \cdot N) \leftrightarrow (M ∥ K \to M \cdot N ∥ K))$
24	20 23	syl5ibcom	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \gcd N = 1 \land x \in ℤ)) \to (x \cdot N = K \to (M ∥ K \to M \cdot N ∥ K))$
25	24	anassrs	$⊢ (((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \gcd N = 1) \land x \in ℤ) \to (x \cdot N = K \to (M ∥ K \to M \cdot N ∥ K))$
26	25	rexlimdva	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \gcd N = 1) \to (\exists x \in ℤ x \cdot N = K \to (M ∥ K \to M \cdot N ∥ K))$
27	3 26	sylbid	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \gcd N = 1) \to (N ∥ K \to (M ∥ K \to M \cdot N ∥ K))$
28	27	impcomd	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \gcd N = 1) \to ((M ∥ K \land N ∥ K) \to M \cdot N ∥ K)$

Metamath Proof Explorer

Theorem coprmdvds2

Proof