Metamath Proof Explorer

Theorem modmulmod

Description: The product of a real number modulo a positive real number and an integer equals the product of the real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

		Ref	Expression
	Assertion	modmulmod	$⊢ (A \in ℝ \land B \in ℤ \land M \in ℝ^{+}) \to (A \mod M) B \mod M = A B \mod M$

Proof

Step	Hyp	Ref	Expression
1		modcl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℝ$
2		simpl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \in ℝ$
3	1 2	jca	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M \in ℝ \land A \in ℝ)$
4	3	3adant2	$⊢ (A \in ℝ \land B \in ℤ \land M \in ℝ^{+}) \to (A \mod M \in ℝ \land A \in ℝ)$
5		3simpc	$⊢ (A \in ℝ \land B \in ℤ \land M \in ℝ^{+}) \to (B \in ℤ \land M \in ℝ^{+})$
6		modabs2	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M) \mod M = A \mod M$
7	6	3adant2	$⊢ (A \in ℝ \land B \in ℤ \land M \in ℝ^{+}) \to (A \mod M) \mod M = A \mod M$
8		modmul1	$⊢ ((A \mod M \in ℝ \land A \in ℝ) \land (B \in ℤ \land M \in ℝ^{+}) \land (A \mod M) \mod M = A \mod M) \to (A \mod M) B \mod M = A B \mod M$
9	4 5 7 8	syl3anc	$⊢ (A \in ℝ \land B \in ℤ \land M \in ℝ^{+}) \to (A \mod M) B \mod M = A B \mod M$