# 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\left({B}\mathrm{mod}{M}\right)\mathrm{mod}{M}={A}{B}\mathrm{mod}{M}$

### Proof

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