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 ) )