Metamath Proof Explorer

Theorem nndivides

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

Ref Expression
Assertion nndivides ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∥ N ↔ ∃ n ∈ ℕ n ⋅ M = N

Proof

Step Hyp Ref Expression
1 nndiv ⊢ M ∈ ℕ ∧ N ∈ ℕ → ∃ n ∈ ℕ M ⁢ n = N ↔ N M ∈ ℕ
2 nncn ⊢ n ∈ ℕ → n ∈ ℂ
3 2 adantl ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ n ∈ ℕ → n ∈ ℂ
4 nncn ⊢ M ∈ ℕ → M ∈ ℂ
5 4 ad2antrr ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ n ∈ ℕ → M ∈ ℂ
6 3 5 mulcomd ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ n ∈ ℕ → n ⋅ M = M ⁢ n
7 6 eqeq1d ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ n ∈ ℕ → n ⋅ M = N ↔ M ⁢ n = N
8 7 rexbidva ⊢ M ∈ ℕ ∧ N ∈ ℕ → ∃ n ∈ ℕ n ⋅ M = N ↔ ∃ n ∈ ℕ M ⁢ n = N
9 nndivdvds ⊢ N ∈ ℕ ∧ M ∈ ℕ → M ∥ N ↔ N M ∈ ℕ
10 9 ancoms ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∥ N ↔ N M ∈ ℕ
11 1 8 10 3bitr4rd ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∥ N ↔ ∃ n ∈ ℕ n ⋅ M = N