muldvds1

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

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

Proof

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		3simpb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℤ \land N \in ℤ)$
5		zmulcl	$⊢ (x \in ℤ \land M \in ℤ) \to x \cdot M \in ℤ$
6	5	ancoms	$⊢ (M \in ℤ \land x \in ℤ) \to x \cdot M \in ℤ$
7	6	3ad2antl2	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to x \cdot M \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		mul32	$⊢ (x \in ℂ \land K \in ℂ \land M \in ℂ) \to x K \cdot M = x \cdot M K$
13	11 12	eqtr3d	$⊢ (x \in ℂ \land K \in ℂ \land M \in ℂ) \to x K \cdot M = x \cdot M K$
14	8 9 10 13	syl3an	$⊢ (x \in ℤ \land K \in ℤ \land M \in ℤ) \to x K \cdot M = x \cdot M K$
15	14	3coml	$⊢ (K \in ℤ \land M \in ℤ \land x \in ℤ) \to x K \cdot M = x \cdot M K$
16	15	3expa	$⊢ ((K \in ℤ \land M \in ℤ) \land x \in ℤ) \to x K \cdot M = x \cdot M K$
17	16	3adantl3	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to x K \cdot M = x \cdot M K$
18	17	eqeq1d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to (x K \cdot M = N \leftrightarrow x \cdot M K = N)$
19	18	biimpd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to (x K \cdot M = N \to x \cdot M K = N)$
20	3 4 7 19	dvds1lem	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \cdot M ∥ N \to K ∥ N)$

Metamath Proof Explorer

Theorem muldvds1

Proof