Theorem dvdssub

Description: An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Assertion	dvdssub	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( M - N ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsnegb	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || -u N ) )
2		znegcl	|- ( N e. ZZ -> -u N e. ZZ )
3		dvdsadd	|- ( ( M e. ZZ /\ -u N e. ZZ ) -> ( M || -u N <-> M || ( M + -u N ) ) )
4	2 3	sylan2	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || -u N <-> M || ( M + -u N ) ) )
5		zcn	|- ( M e. ZZ -> M e. CC )
6		zcn	|- ( N e. ZZ -> N e. CC )
7		negsub	|- ( ( M e. CC /\ N e. CC ) -> ( M + -u N ) = ( M - N ) )
8	5 6 7	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + -u N ) = ( M - N ) )
9	8	breq2d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M + -u N ) <-> M || ( M - N ) ) )
10	1 4 9	3bitrd	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( M - N ) ) )