Metamath Proof Explorer


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 MNMNnn M=N

Proof

Step Hyp Ref Expression
1 df-br MNMN
2 df-dvds =xy|xynnx=y
3 2 eleq2i MNMNxy|xynnx=y
4 1 3 bitri MNMNxy|xynnx=y
5 oveq2 x=Mnx=n M
6 5 eqeq1d x=Mnx=yn M=y
7 6 rexbidv x=Mnnx=ynn M=y
8 eqeq2 y=Nn M=yn M=N
9 8 rexbidv y=Nnn M=ynn M=N
10 7 9 opelopab2 MNMNxy|xynnx=ynn M=N
11 4 10 syl5bb MNMNnn M=N