Metamath Proof Explorer

Theorem divides

Description: Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 ( ex-dvds ). As proven in dvdsval3 , M || N <-> ( N mod M ) = 0 . See divides and dvdsval2 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion divides ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ ∃ n ∈ ℤ n ⋅ M = N

Proof

Step Hyp Ref Expression
1 df-br ⊢ M ∥ N ↔ M N ∈ ∥
2 df-dvds ⊢ ∥ = x y | x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y
3 2 eleq2i ⊢ M N ∈ ∥ ↔ M N ∈ x y | x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y
4 1 3 bitri ⊢ M ∥ N ↔ M N ∈ x y | x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y
5 oveq2 ⊢ x = M → n ⁢ x = n ⋅ M
6 5 eqeq1d ⊢ x = M → n ⁢ x = y ↔ n ⋅ M = y
7 6 rexbidv ⊢ x = M → ∃ n ∈ ℤ n ⁢ x = y ↔ ∃ n ∈ ℤ n ⋅ M = y
8 eqeq2 ⊢ y = N → n ⋅ M = y ↔ n ⋅ M = N
9 8 rexbidv ⊢ y = N → ∃ n ∈ ℤ n ⋅ M = y ↔ ∃ n ∈ ℤ n ⋅ M = N
10 7 9 opelopab2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M N ∈ x y | x ∈ ℤ ∧ y ∈ ℤ ∧ ∃ n ∈ ℤ n ⁢ x = y ↔ ∃ n ∈ ℤ n ⋅ M = N
11 4 10 bitrid ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ ∃ n ∈ ℤ n ⋅ M = N