Step |
Hyp |
Ref |
Expression |
1 |
|
nnz |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ ) |
2 |
|
nnne0 |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 ) |
3 |
1 2
|
jca |
⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) |
4 |
|
dvdsval2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) |
5 |
4
|
3expa |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) |
6 |
3 5
|
sylan |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) |
7 |
|
zre |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ ) |
8 |
|
nnrp |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ+ ) |
9 |
|
mod0 |
⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝑁 mod 𝑀 ) = 0 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) |
10 |
7 8 9
|
syl2anr |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 mod 𝑀 ) = 0 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) ) |
11 |
6 10
|
bitr4d |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 mod 𝑀 ) = 0 ) ) |