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 | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑁 ∥ 𝐴 → ( ( 𝐴 · 𝐵 ) mod 𝑁 ) = 0 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1 | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝑁 ∈ ℕ ) | |
| 2 | nnz | ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ ) | |
| 3 | dvdsmultr1 | ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑁 ∥ 𝐴 → 𝑁 ∥ ( 𝐴 · 𝐵 ) ) ) | |
| 4 | 2 3 | syl3an1 | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑁 ∥ 𝐴 → 𝑁 ∥ ( 𝐴 · 𝐵 ) ) ) |
| 5 | dvdsmod0 | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ∥ ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 · 𝐵 ) mod 𝑁 ) = 0 ) | |
| 6 | 1 4 5 | syl6an | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑁 ∥ 𝐴 → ( ( 𝐴 · 𝐵 ) mod 𝑁 ) = 0 ) ) |