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

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

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝑀 ∥ 𝑁 ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ∥ )
2 df-dvds ⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) }
3 2 eleq2i ⊢ ( ⟨ 𝑀 , 𝑁 ⟩ ∈ ∥ ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) } )
4 1 3 bitri ⊢ ( 𝑀 ∥ 𝑁 ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) } )
5 oveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑛 · 𝑥 ) = ( 𝑛 · 𝑀 ) )
6 5 eqeq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑛 · 𝑥 ) = 𝑦 ↔ ( 𝑛 · 𝑀 ) = 𝑦 ) )
7 6 rexbidv ⊢ ( 𝑥 = 𝑀 → ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑦 ) )
8 eqeq2 ⊢ ( 𝑦 = 𝑁 → ( ( 𝑛 · 𝑀 ) = 𝑦 ↔ ( 𝑛 · 𝑀 ) = 𝑁 ) )
9 8 rexbidv ⊢ ( 𝑦 = 𝑁 → ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑦 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑁 ) )
10 7 9 opelopab2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ⟨ 𝑀 , 𝑁 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑥 ) = 𝑦 ) } ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑁 ) )
11 4 10 bitrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑁 ) )