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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑀 ∥ 𝑁 → 𝑀 ≤ ( abs ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 dvdsabsb ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( abs ‘ 𝑁 ) ) )
2 1 3adant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( abs ‘ 𝑁 ) ) )
3 nnabscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
4 dvdsle ⊢ ( ( 𝑀 ∈ ℤ ∧ ( abs ‘ 𝑁 ) ∈ ℕ ) → ( 𝑀 ∥ ( abs ‘ 𝑁 ) → 𝑀 ≤ ( abs ‘ 𝑁 ) ) )
5 3 4 sylan2 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 ∥ ( abs ‘ 𝑁 ) → 𝑀 ≤ ( abs ‘ 𝑁 ) ) )
6 5 3impb ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑀 ∥ ( abs ‘ 𝑁 ) → 𝑀 ≤ ( abs ‘ 𝑁 ) ) )
7 2 6 sylbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑀 ∥ 𝑁 → 𝑀 ≤ ( abs ‘ 𝑁 ) ) )