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

Metamath Proof Explorer

Theorem dvdsnegb

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

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ZZ /\ N e. ZZ ) )
2 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
3 2 anim2i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ZZ /\ -u 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 mulneg1 
 |-  ( ( x e. CC /\ M e. CC ) -> ( -u x x. M ) = -u ( x x. M ) )
9 negeq 
 |-  ( ( x x. M ) = N -> -u ( x x. M ) = -u N )
10 9 eqeq2d 
 |-  ( ( x x. M ) = N -> ( ( -u x x. M ) = -u ( x x. M ) <-> ( -u x x. M ) = -u N ) )
11 8 10 syl5ibcom 
 |-  ( ( x e. CC /\ M e. CC ) -> ( ( x x. M ) = N -> ( -u x x. M ) = -u N ) )
12 6 7 11 syl2anr 
 |-  ( ( M e. ZZ /\ x e. ZZ ) -> ( ( x x. M ) = N -> ( -u x x. M ) = -u N ) )
13 12 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. M ) = N -> ( -u x x. M ) = -u N ) )
14 1 3 5 13 dvds1lem 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> M || -u N ) )
15 zcn 
 |-  ( N e. ZZ -> N e. CC )
16 negeq 
 |-  ( ( x x. M ) = -u N -> -u ( x x. M ) = -u -u N )
17 negneg 
 |-  ( N e. CC -> -u -u N = N )
18 16 17 sylan9eqr 
 |-  ( ( N e. CC /\ ( x x. M ) = -u N ) -> -u ( x x. M ) = N )
19 8 18 sylan9eq 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ ( N e. CC /\ ( x x. M ) = -u N ) ) -> ( -u x x. M ) = N )
20 19 expr 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ N e. CC ) -> ( ( x x. M ) = -u N -> ( -u x x. M ) = N ) )
21 20 3impa 
 |-  ( ( x e. CC /\ M e. CC /\ N e. CC ) -> ( ( x x. M ) = -u N -> ( -u x x. M ) = N ) )
22 6 7 15 21 syl3an 
 |-  ( ( x e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( x x. M ) = -u N -> ( -u x x. M ) = N ) )
23 22 3coml 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ x e. ZZ ) -> ( ( x x. M ) = -u N -> ( -u x x. M ) = N ) )
24 23 3expa 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. M ) = -u N -> ( -u x x. M ) = N ) )
25 3 1 5 24 dvds1lem 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || -u N -> M || N ) )
26 14 25 impbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || -u N ) )