Theorem dvdsadd

Description: An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 13-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
2		zaddcl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
3		simpr	|- ( ( M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
4		iddvds	|- ( M e. ZZ -> M || M )
5	4	adantr	|- ( ( M e. ZZ /\ N e. ZZ ) -> M || M )
6		zcn	|- ( M e. ZZ -> M e. CC )
7		zcn	|- ( N e. ZZ -> N e. CC )
8		pncan	|- ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - N ) = M )
9	6 7 8	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + N ) - N ) = M )
10	5 9	breqtrrd	|- ( ( M e. ZZ /\ N e. ZZ ) -> M || ( ( M + N ) - N ) )
11		dvdssub2	|- ( ( ( M e. ZZ /\ ( M + N ) e. ZZ /\ N e. ZZ ) /\ M || ( ( M + N ) - N ) ) -> ( M || ( M + N ) <-> M || N ) )
12	1 2 3 10 11	syl31anc	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M + N ) <-> M || N ) )
13	12	bicomd	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( M + N ) ) )