dvdsmultr2

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

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

Step	Hyp	Ref	Expression
1		dvdsmul2	$⊢ (M \in ℤ \land N \in ℤ) \to N ∥ M \cdot N$
2	1	biantrud	$⊢ (M \in ℤ \land N \in ℤ) \to (K ∥ N \leftrightarrow (K ∥ N \land N ∥ M \cdot N))$
3	2	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ N \leftrightarrow (K ∥ N \land N ∥ M \cdot N))$
4		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
5		simp3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to N \in ℤ$
6		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
7	6	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
8		dvdstr	$⊢ (K \in ℤ \land N \in ℤ \land M \cdot N \in ℤ) \to ((K ∥ N \land N ∥ M \cdot N) \to K ∥ M \cdot N)$
9	4 5 7 8	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ N \land N ∥ M \cdot N) \to K ∥ M \cdot N)$
10	3 9	sylbid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ N \to K ∥ M \cdot N)$

Metamath Proof Explorer