dvdsmultr1

Description: If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012)

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

Step	Hyp	Ref	Expression
1		dvdsmul1	$⊢ (M \in ℤ \land N \in ℤ) \to M ∥ M \cdot N$
2	1	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M ∥ M \cdot N$
3		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
4	3	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
5		dvdstr	$⊢ (K \in ℤ \land M \in ℤ \land M \cdot N \in ℤ) \to ((K ∥ M \land M ∥ M \cdot N) \to K ∥ M \cdot N)$
6	4 5	syld3an3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land M ∥ M \cdot N) \to K ∥ M \cdot N)$
7	2 6	mpan2d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ M \to K ∥ M \cdot N)$

Metamath Proof Explorer