Theorem dvdssubr

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

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

Proof

Step	Hyp	Ref	Expression
1		zsubcl	|- ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
2	1	ancoms	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N - M ) e. ZZ )
3		dvdsadd	|- ( ( M e. ZZ /\ ( N - M ) e. ZZ ) -> ( M || ( N - M ) <-> M || ( M + ( N - M ) ) ) )
4	2 3	syldan	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( N - M ) <-> M || ( M + ( N - M ) ) ) )
5		zcn	|- ( M e. ZZ -> M e. CC )
6		zcn	|- ( N e. ZZ -> N e. CC )
7		pncan3	|- ( ( M e. CC /\ N e. CC ) -> ( M + ( N - M ) ) = N )
8	5 6 7	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + ( N - M ) ) = N )
9	8	breq2d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M + ( N - M ) ) <-> M || N ) )
10	4 9	bitr2d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( N - M ) ) )