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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdsabsb | |
|
2 | 1 | 3adant3 | |
3 | nnabscl | |
|
4 | dvdsle | |
|
5 | 3 4 | sylan2 | |
6 | 5 | 3impb | |
7 | 2 6 | sylbid | |