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 ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N → M ≤ N

Proof

Step Hyp Ref Expression
1 dvdsabsb ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N
2 1 3adant3 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N ↔ M ∥ N
3 nnabscl ⊢ N ∈ ℤ ∧ N ≠ 0 → N ∈ ℕ
4 dvdsle ⊢ M ∈ ℤ ∧ N ∈ ℕ → M ∥ N → M ≤ N
5 3 4 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N → M ≤ N
6 5 3impb ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N → M ≤ N
7 2 6 sylbid ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N → M ≤ N