This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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