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