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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br | |
|
2 | df-dvds | |
|
3 | 2 | eleq2i | |
4 | 1 3 | bitri | |
5 | oveq2 | |
|
6 | 5 | eqeq1d | |
7 | 6 | rexbidv | |
8 | eqeq2 | |
|
9 | 8 | rexbidv | |
10 | 7 9 | opelopab2 | |
11 | 4 10 | syl5bb | |