This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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