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	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 − 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3simpa	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
2		3simpb	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
3		zsubcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
4	3	anim2i	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐾 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) )
5	4	3impb	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) )
6		zsubcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 − 𝑦 ) ∈ ℤ )
7	6	adantl	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 − 𝑦 ) ∈ ℤ )
8		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
9		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
10		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
11		subdir	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) )
12	8 9 10 11	syl3an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) )
13	12	3comr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) )
14	13	3expb	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) )
15		oveq12	⊢ ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) → ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) = ( 𝑀 − 𝑁 ) )
16	14 15	sylan9eq	⊢ ( ( ( 𝐾 ∈ ℤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( 𝑀 − 𝑁 ) )
17	16	ex	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( 𝑀 − 𝑁 ) ) )
18	17	3ad2antl1	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( 𝑀 − 𝑁 ) ) )
19	1 2 5 7 18	dvds2lem	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 − 𝑁 ) ) )