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

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