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 | |- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( N || A -> ( ( A x. B ) mod N ) = 0 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1 | |- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> N e. NN ) |
|
| 2 | nnz | |- ( N e. NN -> N e. ZZ ) |
|
| 3 | dvdsmultr1 | |- ( ( N e. ZZ /\ A e. ZZ /\ B e. ZZ ) -> ( N || A -> N || ( A x. B ) ) ) |
|
| 4 | 2 3 | syl3an1 | |- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( N || A -> N || ( A x. B ) ) ) |
| 5 | dvdsmod0 | |- ( ( N e. NN /\ N || ( A x. B ) ) -> ( ( A x. B ) mod N ) = 0 ) |
|
| 6 | 1 4 5 | syl6an | |- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( N || A -> ( ( A x. B ) mod N ) = 0 ) ) |