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 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → N ∥ A → A ⁢ B mod N = 0

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → N ∈ ℕ
2 nnz ⊢ N ∈ ℕ → N ∈ ℤ
3 dvdsmultr1 ⊢ N ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ → N ∥ A → N ∥ A ⁢ B
4 2 3 syl3an1 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → N ∥ A → N ∥ A ⁢ B
5 dvdsmod0 ⊢ N ∈ ℕ ∧ N ∥ A ⁢ B → A ⁢ B mod N = 0
6 1 4 5 syl6an ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → N ∥ A → A ⁢ B mod N = 0