This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℕ \land A \in ℤ \land B \in ℤ) \to (N ∥ A \to A B \mod N = 0)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land A \in ℤ \land B \in ℤ) \to N \in ℕ$
2		nnz	$⊢ N \in ℕ \to N \in ℤ$
3		dvdsmultr1	$⊢ (N \in ℤ \land A \in ℤ \land B \in ℤ) \to (N ∥ A \to N ∥ A B)$
4	2 3	syl3an1	$⊢ (N \in ℕ \land A \in ℤ \land B \in ℤ) \to (N ∥ A \to N ∥ A B)$
5		dvdsmod0	$⊢ (N \in ℕ \land N ∥ A B) \to A B \mod N = 0$
6	1 4 5	syl6an	$⊢ (N \in ℕ \land A \in ℤ \land B \in ℤ) \to (N ∥ A \to A B \mod N = 0)$