dvdsmul1

Description: An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011)

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

Step	Hyp	Ref	Expression
1		zcn	$⊢ N \in ℤ \to N \in ℂ$
2		zcn	$⊢ M \in ℤ \to M \in ℂ$
3		mulcom	$⊢ (N \in ℂ \land M \in ℂ) \to N \cdot M = M \cdot N$
4	1 2 3	syl2anr	$⊢ (M \in ℤ \land N \in ℤ) \to N \cdot M = M \cdot N$
5		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
6		dvds0lem	$⊢ ((N \in ℤ \land M \in ℤ \land M \cdot N \in ℤ) \land N \cdot M = M \cdot N) \to M ∥ M \cdot N$
7	6	ex	$⊢ (N \in ℤ \land M \in ℤ \land M \cdot N \in ℤ) \to (N \cdot M = M \cdot N \to M ∥ M \cdot N)$
8	7	3com12	$⊢ (M \in ℤ \land N \in ℤ \land M \cdot N \in ℤ) \to (N \cdot M = M \cdot N \to M ∥ M \cdot N)$
9	5 8	mpd3an3	$⊢ (M \in ℤ \land N \in ℤ) \to (N \cdot M = M \cdot N \to M ∥ M \cdot N)$
10	4 9	mpd	$⊢ (M \in ℤ \land N \in ℤ) \to M ∥ M \cdot N$

Metamath Proof Explorer