Step |
Hyp |
Ref |
Expression |
1 |
|
nndiv |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ( 𝑀 · 𝑛 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℕ ) ) |
2 |
|
nncn |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ ) |
3 |
2
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ ) |
4 |
|
nncn |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ ) |
5 |
4
|
ad2antrr |
⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ℂ ) |
6 |
3 5
|
mulcomd |
⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · 𝑀 ) = ( 𝑀 · 𝑛 ) ) |
7 |
6
|
eqeq1d |
⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 · 𝑀 ) = 𝑁 ↔ ( 𝑀 · 𝑛 ) = 𝑁 ) ) |
8 |
7
|
rexbidva |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( 𝑀 · 𝑛 ) = 𝑁 ) ) |
9 |
|
nndivdvds |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℕ ) ) |
10 |
9
|
ancoms |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℕ ) ) |
11 |
1 8 10
|
3bitr4rd |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ) ) |