Metamath Proof Explorer

Theorem dvdsleabs2

Description: Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014)

Ref Expression
Assertion dvdsleabs2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N → M ≤ N

Proof

Step Hyp Ref Expression
1 zabscl ⊢ M ∈ ℤ → M ∈ ℤ
2 1 3anim1i ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0
3 2 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ M ∥ N → M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0
4 absdvdsb ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ N
5 4 3adant3 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N ↔ M ∥ N
6 5 biimpa ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ M ∥ N → M ∥ N
7 dvdsleabs ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N → M ≤ N
8 3 6 7 sylc ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ M ∥ N → M ≤ N
9 8 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∥ N → M ≤ N