Metamath Proof Explorer

Theorem dvdsabsb

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

Ref Expression
Assertion dvdsabsb 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( abs ` N ) ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( ( abs ` N ) = N -> ( M || ( abs ` N ) <-> M || N ) )
2 1 bicomd 
 |-  ( ( abs ` N ) = N -> ( M || N <-> M || ( abs ` N ) ) )
3 2 a1i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` N ) = N -> ( M || N <-> M || ( abs ` N ) ) ) )
4 dvdsnegb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || -u N ) )
5 breq2 
 |-  ( ( abs ` N ) = -u N -> ( M || ( abs ` N ) <-> M || -u N ) )
6 5 bicomd 
 |-  ( ( abs ` N ) = -u N -> ( M || -u N <-> M || ( abs ` N ) ) )
7 4 6 sylan9bb 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( abs ` N ) = -u N ) -> ( M || N <-> M || ( abs ` N ) ) )
8 7 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` N ) = -u N -> ( M || N <-> M || ( abs ` N ) ) ) )
9 zre 
 |-  ( N e. ZZ -> N e. RR )
10 9 absord 
 |-  ( N e. ZZ -> ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) )
11 10 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) )
12 3 8 11 mpjaod 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( abs ` N ) ) )