Metamath Proof Explorer


Theorem mulmoddvds

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 NABNAABmodN=0

Proof

Step Hyp Ref Expression
1 simp1 NABN
2 nnz NN
3 dvdsmultr1 NABNANAB
4 2 3 syl3an1 NABNANAB
5 dvdsmod0 NNABABmodN=0
6 1 4 5 syl6an NABNAABmodN=0