Metamath Proof Explorer

Theorem dvdssub2

Description: If an integer divides a difference, then it divides one term iff it divides the other. (Contributed by Mario Carneiro, 13-Jul-2014)

Ref Expression
Assertion dvdssub2 ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ ( 𝑀 − 𝑁 ) ) → ( 𝐾 ∥ 𝑀 ↔ 𝐾 ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
2 1 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
3 dvds2sub ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ ( 𝑀 − 𝑁 ) ) → 𝐾 ∥ ( 𝑀 − ( 𝑀 − 𝑁 ) ) ) )
4 2 3 syld3an3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ ( 𝑀 − 𝑁 ) ) → 𝐾 ∥ ( 𝑀 − ( 𝑀 − 𝑁 ) ) ) )
5 4 ancomsd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑀 ) → 𝐾 ∥ ( 𝑀 − ( 𝑀 − 𝑁 ) ) ) )
6 5 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑀 ) ) → 𝐾 ∥ ( 𝑀 − ( 𝑀 − 𝑁 ) ) )
7 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
9 nncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 − ( 𝑀 − 𝑁 ) ) = 𝑁 )
10 7 8 9 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − ( 𝑀 − 𝑁 ) ) = 𝑁 )
11 10 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − ( 𝑀 − 𝑁 ) ) = 𝑁 )
12 11 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑀 ) ) → ( 𝑀 − ( 𝑀 − 𝑁 ) ) = 𝑁 )
13 6 12 breqtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑀 ) ) → 𝐾 ∥ 𝑁 )
14 13 expr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ ( 𝑀 − 𝑁 ) ) → ( 𝐾 ∥ 𝑀 → 𝐾 ∥ 𝑁 ) )
15 dvds2add ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( ( 𝑀 − 𝑁 ) + 𝑁 ) ) )
16 2 15 syld3an2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( ( 𝑀 − 𝑁 ) + 𝑁 ) ) )
17 16 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) ) → 𝐾 ∥ ( ( 𝑀 − 𝑁 ) + 𝑁 ) )
18 npcan ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 − 𝑁 ) + 𝑁 ) = 𝑀 )
19 7 8 18 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 − 𝑁 ) + 𝑁 ) = 𝑀 )
20 19 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 − 𝑁 ) + 𝑁 ) = 𝑀 )
21 20 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) ) → ( ( 𝑀 − 𝑁 ) + 𝑁 ) = 𝑀 )
22 17 21 breqtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ ( 𝑀 − 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) ) → 𝐾 ∥ 𝑀 )
23 22 expr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ ( 𝑀 − 𝑁 ) ) → ( 𝐾 ∥ 𝑁 → 𝐾 ∥ 𝑀 ) )
24 14 23 impbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ ( 𝑀 − 𝑁 ) ) → ( 𝐾 ∥ 𝑀 ↔ 𝐾 ∥ 𝑁 ) )