Description: If an integer is divisible by a positive integer, the product of this integer with another integer modulo the positive integer is 0. (Contributed by Alexander van der Vekens, 30-Aug-2018) (Proof shortened by AV, 18-Mar-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | mulmoddvds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | nnz | |
|
3 | dvdsmultr1 | |
|
4 | 2 3 | syl3an1 | |
5 | dvdsmod0 | |
|
6 | 1 4 5 | syl6an | |