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

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 e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || ( M - N ) ) -> ( K || M <-> K || N ) )

Proof

Step Hyp Ref Expression
1 zsubcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
2 1 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
3 dvds2sub 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ ( M - N ) e. ZZ ) -> ( ( K || M /\ K || ( M - N ) ) -> K || ( M - ( M - N ) ) ) )
4 2 3 syld3an3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || ( M - N ) ) -> K || ( M - ( M - N ) ) ) )
5 4 ancomsd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( M - N ) /\ K || M ) -> K || ( M - ( M - N ) ) ) )
6 5 imp 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || ( M - N ) /\ K || M ) ) -> K || ( M - ( M - N ) ) )
7 zcn 
 |-  ( M e. ZZ -> M e. CC )
8 zcn 
 |-  ( N e. ZZ -> N e. CC )
9 nncan 
 |-  ( ( M e. CC /\ N e. CC ) -> ( M - ( M - N ) ) = N )
10 7 8 9 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M - ( M - N ) ) = N )
11 10 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M - ( M - N ) ) = N )
12 11 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || ( M - N ) /\ K || M ) ) -> ( M - ( M - N ) ) = N )
13 6 12 breqtrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || ( M - N ) /\ K || M ) ) -> K || N )
14 13 expr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || ( M - N ) ) -> ( K || M -> K || N ) )
15 dvds2add 
 |-  ( ( K e. ZZ /\ ( M - N ) e. ZZ /\ N e. ZZ ) -> ( ( K || ( M - N ) /\ K || N ) -> K || ( ( M - N ) + N ) ) )
16 2 15 syld3an2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( M - N ) /\ K || N ) -> K || ( ( M - N ) + N ) ) )
17 16 imp 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || ( M - N ) /\ K || N ) ) -> K || ( ( M - N ) + N ) )
18 npcan 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M - N ) + N ) = M )
19 7 8 18 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M - N ) + N ) = M )
20 19 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M - N ) + N ) = M )
21 20 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || ( M - N ) /\ K || N ) ) -> ( ( M - N ) + N ) = M )
22 17 21 breqtrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || ( M - N ) /\ K || N ) ) -> K || M )
23 22 expr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || ( M - N ) ) -> ( K || N -> K || M ) )
24 14 23 impbid 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || ( M - N ) ) -> ( K || M <-> K || N ) )