Theorem dvdsaddr

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

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

Proof

Step	Hyp	Ref	Expression
1		dvdsadd	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( M + N ) ) )
2		zcn	|- ( M e. ZZ -> M e. CC )
3		zcn	|- ( N e. ZZ -> N e. CC )
4		addcom	|- ( ( M e. CC /\ N e. CC ) -> ( M + N ) = ( N + M ) )
5	2 3 4	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) = ( N + M ) )
6	5	breq2d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M + N ) <-> M || ( N + M ) ) )
7	1 6	bitrd	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( N + M ) ) )