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

Metamath Proof Explorer

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