This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )