dvdsmulc

Description: Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step	Hyp	Ref	Expression
1		3simpc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M \in ℤ \land N \in ℤ)$
2		zmulcl	$⊢ (M \in ℤ \land K \in ℤ) \to M K \in ℤ$
3	2	3adant2	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to M K \in ℤ$
4		zmulcl	$⊢ (N \in ℤ \land K \in ℤ) \to N K \in ℤ$
5	4	3adant1	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to N K \in ℤ$
6	3 5	jca	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M K \in ℤ \land N K \in ℤ)$
7	6	3comr	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M K \in ℤ \land N K \in ℤ)$
8		simpr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to x \in ℤ$
9		zcn	$⊢ x \in ℤ \to x \in ℂ$
10		zcn	$⊢ M \in ℤ \to M \in ℂ$
11		zcn	$⊢ K \in ℤ \to K \in ℂ$
12		mulass	$⊢ (x \in ℂ \land M \in ℂ \land K \in ℂ) \to x \cdot M K = x M K$
13	9 10 11 12	syl3an	$⊢ (x \in ℤ \land M \in ℤ \land K \in ℤ) \to x \cdot M K = x M K$
14	13	3com13	$⊢ (K \in ℤ \land M \in ℤ \land x \in ℤ) \to x \cdot M K = x M K$
15	14	3expa	$⊢ ((K \in ℤ \land M \in ℤ) \land x \in ℤ) \to x \cdot M K = x M K$
16	15	3adantl3	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to x \cdot M K = x M K$
17		oveq1	$⊢ x \cdot M = N \to x \cdot M K = N K$
18	16 17	sylan9req	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \land x \cdot M = N) \to x M K = N K$
19	18	ex	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land x \in ℤ) \to (x \cdot M = N \to x M K = N K)$
20	1 7 8 19	dvds1lem	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M ∥ N \to M K ∥ N K)$
21	20	3coml	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M ∥ N \to M K ∥ N K)$

Metamath Proof Explorer

Theorem dvdsmulc

Proof