# Metamath Proof Explorer

## Theorem moddi

Description: Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008)

Ref Expression
Assertion moddi ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\left({B}\mathrm{mod}{C}\right)={A}{B}\mathrm{mod}{A}{C}$

### Proof

Step Hyp Ref Expression
1 rpcn ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℂ$
2 1 3ad2ant1 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\in ℂ$
3 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
4 3 3ad2ant2 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\in ℂ$
5 rpre ${⊢}{C}\in {ℝ}^{+}\to {C}\in ℝ$
6 5 adantl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in ℝ$
7 refldivcl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℝ$
8 6 7 remulcld ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{B}}{{C}}⌋\in ℝ$
9 8 recnd ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{B}}{{C}}⌋\in ℂ$
10 9 3adant1 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{B}}{{C}}⌋\in ℂ$
11 2 4 10 subdid ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\left({B}-{C}⌊\frac{{B}}{{C}}⌋\right)={A}{B}-{A}{C}⌊\frac{{B}}{{C}}⌋$
12 rpcnne0 ${⊢}{C}\in {ℝ}^{+}\to \left({C}\in ℂ\wedge {C}\ne 0\right)$
13 12 3ad2ant3 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({C}\in ℂ\wedge {C}\ne 0\right)$
14 rpcnne0 ${⊢}{A}\in {ℝ}^{+}\to \left({A}\in ℂ\wedge {A}\ne 0\right)$
15 14 3ad2ant1 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\in ℂ\wedge {A}\ne 0\right)$
16 divcan5 ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\wedge \left({A}\in ℂ\wedge {A}\ne 0\right)\right)\to \frac{{A}{B}}{{A}{C}}=\frac{{B}}{{C}}$
17 4 13 15 16 syl3anc ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \frac{{A}{B}}{{A}{C}}=\frac{{B}}{{C}}$
18 17 fveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{A}{B}}{{A}{C}}⌋=⌊\frac{{B}}{{C}}⌋$
19 18 oveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}{C}⌊\frac{{A}{B}}{{A}{C}}⌋={A}{C}⌊\frac{{B}}{{C}}⌋$
20 rpcn ${⊢}{C}\in {ℝ}^{+}\to {C}\in ℂ$
21 20 3ad2ant3 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in ℂ$
22 rerpdivcl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \frac{{B}}{{C}}\in ℝ$
23 reflcl ${⊢}\frac{{B}}{{C}}\in ℝ\to ⌊\frac{{B}}{{C}}⌋\in ℝ$
24 23 recnd ${⊢}\frac{{B}}{{C}}\in ℝ\to ⌊\frac{{B}}{{C}}⌋\in ℂ$
25 22 24 syl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℂ$
26 25 3adant1 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℂ$
27 2 21 26 mulassd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}{C}⌊\frac{{B}}{{C}}⌋={A}{C}⌊\frac{{B}}{{C}}⌋$
28 19 27 eqtr2d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}{C}⌊\frac{{B}}{{C}}⌋={A}{C}⌊\frac{{A}{B}}{{A}{C}}⌋$
29 28 oveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}{B}-{A}{C}⌊\frac{{B}}{{C}}⌋={A}{B}-{A}{C}⌊\frac{{A}{B}}{{A}{C}}⌋$
30 11 29 eqtrd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\left({B}-{C}⌊\frac{{B}}{{C}}⌋\right)={A}{B}-{A}{C}⌊\frac{{A}{B}}{{A}{C}}⌋$
31 modval ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}={B}-{C}⌊\frac{{B}}{{C}}⌋$
32 31 3adant1 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}={B}-{C}⌊\frac{{B}}{{C}}⌋$
33 32 oveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\left({B}\mathrm{mod}{C}\right)={A}\left({B}-{C}⌊\frac{{B}}{{C}}⌋\right)$
34 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
35 remulcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}\in ℝ$
36 34 35 sylan ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\right)\to {A}{B}\in ℝ$
37 36 3adant3 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}{B}\in ℝ$
38 rpmulcl ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {A}{C}\in {ℝ}^{+}$
39 modval ${⊢}\left({A}{B}\in ℝ\wedge {A}{C}\in {ℝ}^{+}\right)\to {A}{B}\mathrm{mod}{A}{C}={A}{B}-{A}{C}⌊\frac{{A}{B}}{{A}{C}}⌋$
40 37 38 39 3imp3i2an ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}{B}\mathrm{mod}{A}{C}={A}{B}-{A}{C}⌊\frac{{A}{B}}{{A}{C}}⌋$
41 30 33 40 3eqtr4d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\left({B}\mathrm{mod}{C}\right)={A}{B}\mathrm{mod}{A}{C}$