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 MNN0MNMN

Proof

Step Hyp Ref Expression
1 dvdsabsb MNMNMN
2 1 3adant3 MNN0MNMN
3 nnabscl NN0N
4 dvdsle MNMNMN
5 3 4 sylan2 MNN0MNMN
6 5 3impb MNN0MNMN
7 2 6 sylbid MNN0MNMN