muldvds2

Description: If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011)

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

Step	Hyp	Ref	Expression
1		zmulcl	$⊢ (K \in ℤ \land M \in ℤ) \to K \cdot M \in ℤ$
2	1	anim1i	$⊢ ((K \in ℤ \land M \in ℤ) \land N \in ℤ) \to (K \cdot M \in ℤ \land N \in ℤ)$
3	2	3impa	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \cdot M \in ℤ \land N \in ℤ)$
4		3simpc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M \in ℤ \land N \in ℤ)$
5		zmulcl	$⊢ (x \in ℤ \land K \in ℤ) \to x K \in ℤ$
6	5	ancoms	$⊢ (K \in ℤ \land x \in ℤ) \to x K \in ℤ$
7	6	3ad2antl1	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to x K \in ℤ$
8		zcn	$⊢ x \in ℤ \to x \in ℂ$
9		zcn	$⊢ K \in ℤ \to K \in ℂ$
10		zcn	$⊢ M \in ℤ \to M \in ℂ$
11		mulass	$⊢ (x \in ℂ \land K \in ℂ \land M \in ℂ) \to x K \cdot M = x K \cdot M$
12	8 9 10 11	syl3an	$⊢ (x \in ℤ \land K \in ℤ \land M \in ℤ) \to x K \cdot M = x K \cdot M$
13	12	3coml	$⊢ (K \in ℤ \land M \in ℤ \land x \in ℤ) \to x K \cdot M = x K \cdot M$
14	13	3expa	$⊢ ((K \in ℤ \land M \in ℤ) \land x \in ℤ) \to x K \cdot M = x K \cdot M$
15	14	3adantl3	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to x K \cdot M = x K \cdot M$
16	15	eqeq1d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to (x K \cdot M = N \leftrightarrow x K \cdot M = N)$
17	16	biimprd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to (x K \cdot M = N \to x K \cdot M = N)$
18	3 4 7 17	dvds1lem	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \cdot M ∥ N \to M ∥ N)$

Metamath Proof Explorer