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 ‘ 𝑁 ) ) )