Metamath Proof Explorer

Theorem modmulmodr

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

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

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2	1	3ad2ant1	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to A \in ℂ$
3		simp2	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to B \in ℝ$
4		simp3	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to M \in ℝ^{+}$
5	3 4	modcld	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to B \mod M \in ℝ$
6	5	recnd	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to B \mod M \in ℂ$
7	2 6	mulcomd	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to A (B \mod M) = (B \mod M) A$
8	7	oveq1d	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to A (B \mod M) \mod M = (B \mod M) A \mod M$
9		modmulmod	$⊢ (B \in ℝ \land A \in ℤ \land M \in ℝ^{+}) \to (B \mod M) A \mod M = B A \mod M$
10	9	3com12	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to (B \mod M) A \mod M = B A \mod M$
11		recn	$⊢ B \in ℝ \to B \in ℂ$
12	1 11	anim12ci	$⊢ (A \in ℤ \land B \in ℝ) \to (B \in ℂ \land A \in ℂ)$
13	12	3adant3	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to (B \in ℂ \land A \in ℂ)$
14		mulcom	$⊢ (B \in ℂ \land A \in ℂ) \to B A = A B$
15	13 14	syl	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to B A = A B$
16	15	oveq1d	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to B A \mod M = A B \mod M$
17	8 10 16	3eqtrd	$⊢ (A \in ℤ \land B \in ℝ \land M \in ℝ^{+}) \to A (B \mod M) \mod M = A B \mod M$