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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 · ( 𝐵 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐴 · 𝐵 ) mod 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
3		simp2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
4		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ+ )
5	3 4	modcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 mod 𝑀 ) ∈ ℝ )
6	5	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 mod 𝑀 ) ∈ ℂ )
7	2 6	mulcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 mod 𝑀 ) ) = ( ( 𝐵 mod 𝑀 ) · 𝐴 ) )
8	7	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 · ( 𝐵 mod 𝑀 ) ) mod 𝑀 ) = ( ( ( 𝐵 mod 𝑀 ) · 𝐴 ) mod 𝑀 ) )
9		modmulmod	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐵 mod 𝑀 ) · 𝐴 ) mod 𝑀 ) = ( ( 𝐵 · 𝐴 ) mod 𝑀 ) )
10	9	3com12	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐵 mod 𝑀 ) · 𝐴 ) mod 𝑀 ) = ( ( 𝐵 · 𝐴 ) mod 𝑀 ) )
11		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
12	1 11	anim12ci	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
13	12	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
14		mulcom	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
15	13 14	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
16	15	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 · 𝐴 ) mod 𝑀 ) = ( ( 𝐴 · 𝐵 ) mod 𝑀 ) )
17	8 10 16	3eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 · ( 𝐵 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐴 · 𝐵 ) mod 𝑀 ) )