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

Proof

Step	Hyp	Ref	Expression
1		3simpa	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ M e. ZZ ) )
2		3simpb	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ N e. ZZ ) )
3		zsubcl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
4	3	anim2i	|- ( ( K e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( K e. ZZ /\ ( M - N ) e. ZZ ) )
5	4	3impb	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ ( M - N ) e. ZZ ) )
6		zsubcl	|- ( ( x e. ZZ /\ y e. ZZ ) -> ( x - y ) e. ZZ )
7	6	adantl	|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x - y ) e. ZZ )
8		zcn	|- ( x e. ZZ -> x e. CC )
9		zcn	|- ( y e. ZZ -> y e. CC )
10		zcn	|- ( K e. ZZ -> K e. CC )
11		subdir	|- ( ( x e. CC /\ y e. CC /\ K e. CC ) -> ( ( x - y ) x. K ) = ( ( x x. K ) - ( y x. K ) ) )
12	8 9 10 11	syl3an	|- ( ( x e. ZZ /\ y e. ZZ /\ K e. ZZ ) -> ( ( x - y ) x. K ) = ( ( x x. K ) - ( y x. K ) ) )
13	12	3comr	|- ( ( K e. ZZ /\ x e. ZZ /\ y e. ZZ ) -> ( ( x - y ) x. K ) = ( ( x x. K ) - ( y x. K ) ) )
14	13	3expb	|- ( ( K e. ZZ /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x - y ) x. K ) = ( ( x x. K ) - ( y x. K ) ) )
15		oveq12	|- ( ( ( x x. K ) = M /\ ( y x. K ) = N ) -> ( ( x x. K ) - ( y x. K ) ) = ( M - N ) )
16	14 15	sylan9eq	|- ( ( ( K e. ZZ /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( ( x x. K ) = M /\ ( y x. K ) = N ) ) -> ( ( x - y ) x. K ) = ( M - N ) )
17	16	ex	|- ( ( K e. ZZ /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. K ) = M /\ ( y x. K ) = N ) -> ( ( x - y ) x. K ) = ( M - N ) ) )
18	17	3ad2antl1	|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. K ) = M /\ ( y x. K ) = N ) -> ( ( x - y ) x. K ) = ( M - N ) ) )
19	1 2 5 7 18	dvds2lem	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M - N ) ) )