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 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∥ M − N → K ∥ M ↔ K ∥ N

Proof

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