Metamath Proof Explorer

Theorem dvds2sub

Description: If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℤ \land M \in ℤ)$
2		3simpb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℤ \land N \in ℤ)$
3		zsubcl	$⊢ (M \in ℤ \land N \in ℤ) \to M - N \in ℤ$
4	3	anim2i	$⊢ (K \in ℤ \land (M \in ℤ \land N \in ℤ)) \to (K \in ℤ \land M - N \in ℤ)$
5	4	3impb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℤ \land M - N \in ℤ)$
6		zsubcl	$⊢ (x \in ℤ \land y \in ℤ) \to x - y \in ℤ$
7	6	adantl	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (x \in ℤ \land y \in ℤ)) \to x - y \in ℤ$
8		zcn	$⊢ x \in ℤ \to x \in ℂ$
9		zcn	$⊢ y \in ℤ \to y \in ℂ$
10		zcn	$⊢ K \in ℤ \to K \in ℂ$
11		subdir	$⊢ (x \in ℂ \land y \in ℂ \land K \in ℂ) \to (x - y) K = x K - y K$
12	8 9 10 11	syl3an	$⊢ (x \in ℤ \land y \in ℤ \land K \in ℤ) \to (x - y) K = x K - y K$
13	12	3comr	$⊢ (K \in ℤ \land x \in ℤ \land y \in ℤ) \to (x - y) K = x K - y K$
14	13	3expb	$⊢ (K \in ℤ \land (x \in ℤ \land y \in ℤ)) \to (x - y) K = x K - y K$
15		oveq12	$⊢ (x K = M \land y K = N) \to x K - y K = M - N$
16	14 15	sylan9eq	$⊢ ((K \in ℤ \land (x \in ℤ \land y \in ℤ)) \land (x K = M \land y K = N)) \to (x - y) K = M - N$
17	16	ex	$⊢ (K \in ℤ \land (x \in ℤ \land y \in ℤ)) \to ((x K = M \land y K = N) \to (x - y) K = M - N)$
18	17	3ad2antl1	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (x \in ℤ \land y \in ℤ)) \to ((x K = M \land y K = N) \to (x - y) K = M - N)$
19	1 2 5 7 18	dvds2lem	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land K ∥ N) \to K ∥ (M - N))$