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

Metamath Proof Explorer

Theorem dvdsleabs

Description: The divisors of a nonzero integer are bounded by its absolute value. Theorem 1.1(i) in ApostolNT p. 14 (comparison property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011) (Proof shortened by Fan Zheng, 3-Jul-2016)

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

Proof

Step Hyp Ref Expression
1 dvdsabsb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( abs ` N ) ) )
2 1 3adant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N <-> M || ( abs ` N ) ) )
3 nnabscl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
4 dvdsle 
 |-  ( ( M e. ZZ /\ ( abs ` N ) e. NN ) -> ( M || ( abs ` N ) -> M <_ ( abs ` N ) ) )
5 3 4 sylan2 
 |-  ( ( M e. ZZ /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M || ( abs ` N ) -> M <_ ( abs ` N ) ) )
6 5 3impb 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || ( abs ` N ) -> M <_ ( abs ` N ) ) )
7 2 6 sylbid 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N -> M <_ ( abs ` N ) ) )