Metamath Proof Explorer

Theorem modmul1

Description: Multiplication property of the modulo operation. Note that the multiplier C must be an integer. (Contributed by NM, 12-Nov-2008)

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

Proof

Step Hyp Ref Expression
1 modval ${⊢}\left({A}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{D}={A}-{D}⌊\frac{{A}}{{D}}⌋$
2 modval ${⊢}\left({B}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{D}={B}-{D}⌊\frac{{B}}{{D}}⌋$
3 1 2 eqeqan12d ${⊢}\left(\left({A}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\wedge \left({B}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}\mathrm{mod}{D}={B}\mathrm{mod}{D}↔{A}-{D}⌊\frac{{A}}{{D}}⌋={B}-{D}⌊\frac{{B}}{{D}}⌋\right)$
4 3 anandirs ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {D}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{D}={B}\mathrm{mod}{D}↔{A}-{D}⌊\frac{{A}}{{D}}⌋={B}-{D}⌊\frac{{B}}{{D}}⌋\right)$
5 4 adantrl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}\mathrm{mod}{D}={B}\mathrm{mod}{D}↔{A}-{D}⌊\frac{{A}}{{D}}⌋={B}-{D}⌊\frac{{B}}{{D}}⌋\right)$
6 oveq1 ${⊢}{A}-{D}⌊\frac{{A}}{{D}}⌋={B}-{D}⌊\frac{{B}}{{D}}⌋\to \left({A}-{D}⌊\frac{{A}}{{D}}⌋\right){C}=\left({B}-{D}⌊\frac{{B}}{{D}}⌋\right){C}$
7 5 6 syl6bi ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}\mathrm{mod}{D}={B}\mathrm{mod}{D}\to \left({A}-{D}⌊\frac{{A}}{{D}}⌋\right){C}=\left({B}-{D}⌊\frac{{B}}{{D}}⌋\right){C}\right)$
8 rpcn ${⊢}{D}\in {ℝ}^{+}\to {D}\in ℂ$
9 8 ad2antll ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}\in ℂ$
10 zcn ${⊢}{C}\in ℤ\to {C}\in ℂ$
11 10 ad2antrl ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {C}\in ℂ$
12 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to \frac{{A}}{{D}}\in ℝ$
13 12 flcld ${⊢}\left({A}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{D}}⌋\in ℤ$
14 13 zcnd ${⊢}\left({A}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{D}}⌋\in ℂ$
15 14 adantrl ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to ⌊\frac{{A}}{{D}}⌋\in ℂ$
16 9 11 15 mulassd ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}{C}⌊\frac{{A}}{{D}}⌋={D}{C}⌊\frac{{A}}{{D}}⌋$
17 9 11 15 mul32d ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}{C}⌊\frac{{A}}{{D}}⌋={D}⌊\frac{{A}}{{D}}⌋{C}$
18 16 17 eqtr3d ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}{C}⌊\frac{{A}}{{D}}⌋={D}⌊\frac{{A}}{{D}}⌋{C}$
19 18 oveq2d ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋={A}{C}-{D}⌊\frac{{A}}{{D}}⌋{C}$
20 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
21 20 adantr ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {A}\in ℂ$
22 8 adantl ${⊢}\left({A}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to {D}\in ℂ$
23 22 14 mulcld ${⊢}\left({A}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to {D}⌊\frac{{A}}{{D}}⌋\in ℂ$
24 23 adantrl ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}⌊\frac{{A}}{{D}}⌋\in ℂ$
25 21 24 11 subdird ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}-{D}⌊\frac{{A}}{{D}}⌋\right){C}={A}{C}-{D}⌊\frac{{A}}{{D}}⌋{C}$
26 19 25 eqtr4d ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋=\left({A}-{D}⌊\frac{{A}}{{D}}⌋\right){C}$
27 26 adantlr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋=\left({A}-{D}⌊\frac{{A}}{{D}}⌋\right){C}$
28 8 ad2antll ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}\in ℂ$
29 10 ad2antrl ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {C}\in ℂ$
30 rerpdivcl ${⊢}\left({B}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to \frac{{B}}{{D}}\in ℝ$
31 30 flcld ${⊢}\left({B}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{D}}⌋\in ℤ$
32 31 zcnd ${⊢}\left({B}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{D}}⌋\in ℂ$
33 32 adantrl ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to ⌊\frac{{B}}{{D}}⌋\in ℂ$
34 28 29 33 mulassd ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}{C}⌊\frac{{B}}{{D}}⌋={D}{C}⌊\frac{{B}}{{D}}⌋$
35 28 29 33 mul32d ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}{C}⌊\frac{{B}}{{D}}⌋={D}⌊\frac{{B}}{{D}}⌋{C}$
36 34 35 eqtr3d ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}{C}⌊\frac{{B}}{{D}}⌋={D}⌊\frac{{B}}{{D}}⌋{C}$
37 36 oveq2d ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋={B}{C}-{D}⌊\frac{{B}}{{D}}⌋{C}$
38 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
39 38 adantr ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {B}\in ℂ$
40 8 adantl ${⊢}\left({B}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to {D}\in ℂ$
41 40 32 mulcld ${⊢}\left({B}\in ℝ\wedge {D}\in {ℝ}^{+}\right)\to {D}⌊\frac{{B}}{{D}}⌋\in ℂ$
42 41 adantrl ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}⌊\frac{{B}}{{D}}⌋\in ℂ$
43 39 42 29 subdird ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({B}-{D}⌊\frac{{B}}{{D}}⌋\right){C}={B}{C}-{D}⌊\frac{{B}}{{D}}⌋{C}$
44 37 43 eqtr4d ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋=\left({B}-{D}⌊\frac{{B}}{{D}}⌋\right){C}$
45 44 adantll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋=\left({B}-{D}⌊\frac{{B}}{{D}}⌋\right){C}$
46 27 45 eqeq12d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋={B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋↔\left({A}-{D}⌊\frac{{A}}{{D}}⌋\right){C}=\left({B}-{D}⌊\frac{{B}}{{D}}⌋\right){C}\right)$
47 7 46 sylibrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}\mathrm{mod}{D}={B}\mathrm{mod}{D}\to {A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋={B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\right)$
48 oveq1 ${⊢}{A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋={B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\to \left({A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋\right)\mathrm{mod}{D}=\left({B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\right)\mathrm{mod}{D}$
49 zre ${⊢}{C}\in ℤ\to {C}\in ℝ$
50 remulcl ${⊢}\left({A}\in ℝ\wedge {C}\in ℝ\right)\to {A}{C}\in ℝ$
51 49 50 sylan2 ${⊢}\left({A}\in ℝ\wedge {C}\in ℤ\right)\to {A}{C}\in ℝ$
52 51 adantrr ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {A}{C}\in ℝ$
53 simprr ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}\in {ℝ}^{+}$
54 simprl ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {C}\in ℤ$
55 13 adantrl ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to ⌊\frac{{A}}{{D}}⌋\in ℤ$
56 54 55 zmulcld ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {C}⌊\frac{{A}}{{D}}⌋\in ℤ$
57 modcyc2 ${⊢}\left({A}{C}\in ℝ\wedge {D}\in {ℝ}^{+}\wedge {C}⌊\frac{{A}}{{D}}⌋\in ℤ\right)\to \left({A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋\right)\mathrm{mod}{D}={A}{C}\mathrm{mod}{D}$
58 52 53 56 57 syl3anc ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋\right)\mathrm{mod}{D}={A}{C}\mathrm{mod}{D}$
59 58 adantlr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋\right)\mathrm{mod}{D}={A}{C}\mathrm{mod}{D}$
60 remulcl ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to {B}{C}\in ℝ$
61 49 60 sylan2 ${⊢}\left({B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}\in ℝ$
62 61 adantrr ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {B}{C}\in ℝ$
63 simprr ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {D}\in {ℝ}^{+}$
64 simprl ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {C}\in ℤ$
65 31 adantrl ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to ⌊\frac{{B}}{{D}}⌋\in ℤ$
66 64 65 zmulcld ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to {C}⌊\frac{{B}}{{D}}⌋\in ℤ$
67 modcyc2 ${⊢}\left({B}{C}\in ℝ\wedge {D}\in {ℝ}^{+}\wedge {C}⌊\frac{{B}}{{D}}⌋\in ℤ\right)\to \left({B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\right)\mathrm{mod}{D}={B}{C}\mathrm{mod}{D}$
68 62 63 66 67 syl3anc ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\right)\mathrm{mod}{D}={B}{C}\mathrm{mod}{D}$
69 68 adantll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\right)\mathrm{mod}{D}={B}{C}\mathrm{mod}{D}$
70 59 69 eqeq12d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left(\left({A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋\right)\mathrm{mod}{D}=\left({B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\right)\mathrm{mod}{D}↔{A}{C}\mathrm{mod}{D}={B}{C}\mathrm{mod}{D}\right)$
71 48 70 syl5ib ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}{C}-{D}{C}⌊\frac{{A}}{{D}}⌋={B}{C}-{D}{C}⌊\frac{{B}}{{D}}⌋\to {A}{C}\mathrm{mod}{D}={B}{C}\mathrm{mod}{D}\right)$
72 47 71 syld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\right)\to \left({A}\mathrm{mod}{D}={B}\mathrm{mod}{D}\to {A}{C}\mathrm{mod}{D}={B}{C}\mathrm{mod}{D}\right)$
73 72 3impia ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℤ\wedge {D}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{D}={B}\mathrm{mod}{D}\right)\to {A}{C}\mathrm{mod}{D}={B}{C}\mathrm{mod}{D}$