Metamath Proof Explorer


Theorem dvdsr2

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

Ref Expression
Hypotheses dvdsr.1 B=BaseR
dvdsr.2 ˙=rR
dvdsr.3 ·˙=R
Assertion dvdsr2 XBX˙YzBz·˙X=Y

Proof

Step Hyp Ref Expression
1 dvdsr.1 B=BaseR
2 dvdsr.2 ˙=rR
3 dvdsr.3 ·˙=R
4 1 2 3 dvdsr X˙YXBzBz·˙X=Y
5 4 baib XBX˙YzBz·˙X=Y