dvdscmul

Description: Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in ApostolNT p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

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

Metamath Proof Explorer

Theorem dvdscmul

Proof