Metamath Proof Explorer


Theorem nndivides

Description: Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion nndivides ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀𝑁 ↔ ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ) )

Proof

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 ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀𝑁 ↔ ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ) )