This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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