Metamath Proof Explorer

Theorem dvdsabsmod0

Description: Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 24-Sep-2014) (Proof shortened by OpenAI, 3-Jul-2020)

Ref Expression
Assertion dvdsabsmod0 
|- ( ( M e. ZZ /\ N e. ZZ /\ M =/= 0 ) -> ( M || N <-> ( N mod ( abs ` M ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 absdvdsb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )
2 1 adantlr 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )
3 nnabscl 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` M ) e. NN )
4 dvdsval3 
 |-  ( ( ( abs ` M ) e. NN /\ N e. ZZ ) -> ( ( abs ` M ) || N <-> ( N mod ( abs ` M ) ) = 0 ) )
5 3 4 sylan 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( ( abs ` M ) || N <-> ( N mod ( abs ` M ) ) = 0 ) )
6 2 5 bitrd 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( M || N <-> ( N mod ( abs ` M ) ) = 0 ) )
7 6 an32s 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> ( M || N <-> ( N mod ( abs ` M ) ) = 0 ) )
8 7 3impa 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M =/= 0 ) -> ( M || N <-> ( N mod ( abs ` M ) ) = 0 ) )