Metamath Proof Explorer


Theorem dvdszrcl

Description: Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Assertion dvdszrcl XYXY

Proof

Step Hyp Ref Expression
1 df-dvds =xy|xyzzx=y
2 opabssxp xy|xyzzx=y×
3 1 2 eqsstri ×
4 3 brel XYXY