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

Metamath Proof Explorer

Theorem dvdsr2

Description: Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	dvdsr.1	$⊢ B = {Base}_{R}$
	dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	dvdsr.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	dvdsr2	$⊢ X \in B \to (X \underset{˙}{∥} Y \leftrightarrow \exists z \in B z \underset{˙}{\cdot} X = Y)$

Step	Hyp	Ref	Expression
1		dvdsr.1	$⊢ B = {Base}_{R}$
2		dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		dvdsr.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4	1 2 3	dvdsr	$⊢ X \underset{˙}{∥} Y \leftrightarrow (X \in B \land \exists z \in B z \underset{˙}{\cdot} X = Y)$
5	4	baib	$⊢ X \in B \to (X \underset{˙}{∥} Y \leftrightarrow \exists z \in B z \underset{˙}{\cdot} X = Y)$