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