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

Proof

Step	Hyp	Ref	Expression
1		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
2		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
3	1 2	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
4	3	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
5		3simpc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) )
6		modabs2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
7	6	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
8		modmul1	⊢ ( ( ( ( 𝐴 mod 𝑀 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) ) → ( ( ( 𝐴 mod 𝑀 ) · 𝐵 ) mod 𝑀 ) = ( ( 𝐴 · 𝐵 ) mod 𝑀 ) )
9	4 5 7 8	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) · 𝐵 ) mod 𝑀 ) = ( ( 𝐴 · 𝐵 ) mod 𝑀 ) )