Metamath Proof Explorer

Theorem negdvdsb

Description: An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ZZ /\ N e. ZZ ) )
2 znegcl 
 |-  ( M e. ZZ -> -u M e. ZZ )
3 2 anim1i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M e. ZZ /\ N e. ZZ ) )
4 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
5 4 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> -u x e. ZZ )
6 zcn 
 |-  ( x e. ZZ -> x e. CC )
7 zcn 
 |-  ( M e. ZZ -> M e. CC )
8 mul2neg 
 |-  ( ( x e. CC /\ M e. CC ) -> ( -u x x. -u M ) = ( x x. M ) )
9 6 7 8 syl2anr 
 |-  ( ( M e. ZZ /\ x e. ZZ ) -> ( -u x x. -u M ) = ( x x. M ) )
10 9 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( -u x x. -u M ) = ( x x. M ) )
11 10 eqeq1d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( -u x x. -u M ) = N <-> ( x x. M ) = N ) )
12 11 biimprd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. M ) = N -> ( -u x x. -u M ) = N ) )
13 1 3 5 12 dvds1lem 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> -u M || N ) )
14 mulneg12 
 |-  ( ( x e. CC /\ M e. CC ) -> ( -u x x. M ) = ( x x. -u M ) )
15 6 7 14 syl2anr 
 |-  ( ( M e. ZZ /\ x e. ZZ ) -> ( -u x x. M ) = ( x x. -u M ) )
16 15 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( -u x x. M ) = ( x x. -u M ) )
17 16 eqeq1d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( -u x x. M ) = N <-> ( x x. -u M ) = N ) )
18 17 biimprd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. -u M ) = N -> ( -u x x. M ) = N ) )
19 3 1 5 18 dvds1lem 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M || N -> M || N ) )
20 13 19 impbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> -u M || N ) )