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