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 \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow \exists n \in ℤ n \cdot M = N)$

Proof

Step	Hyp	Ref	Expression
1		df-br	$⊢ M ∥ N \leftrightarrow ⟨M, N⟩ \in ∥$
2		df-dvds	$⊢ ∥ = \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)\}$
3	2	eleq2i	$⊢ ⟨M, N⟩ \in ∥ \leftrightarrow ⟨M, N⟩ \in \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)\}$
4	1 3	bitri	$⊢ M ∥ N \leftrightarrow ⟨M, N⟩ \in \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)\}$
5		oveq2	$⊢ x = M \to n x = n \cdot M$
6	5	eqeq1d	$⊢ x = M \to (n x = y \leftrightarrow n \cdot M = y)$
7	6	rexbidv	$⊢ x = M \to (\exists n \in ℤ n x = y \leftrightarrow \exists n \in ℤ n \cdot M = y)$
8		eqeq2	$⊢ y = N \to (n \cdot M = y \leftrightarrow n \cdot M = N)$
9	8	rexbidv	$⊢ y = N \to (\exists n \in ℤ n \cdot M = y \leftrightarrow \exists n \in ℤ n \cdot M = N)$
10	7 9	opelopab2	$⊢ (M \in ℤ \land N \in ℤ) \to (⟨M, N⟩ \in \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)\} \leftrightarrow \exists n \in ℤ n \cdot M = N)$
11	4 10	bitrid	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow \exists n \in ℤ n \cdot M = N)$

Metamath Proof Explorer

Theorem divides

Proof