# Metamath Proof Explorer

## Theorem modsubdir

Description: Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008)

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

### Proof

Step Hyp Ref Expression
1 modcl ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}\in ℝ$
2 1 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}\in ℝ$
3 modcl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}\in ℝ$
4 3 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}\in ℝ$
5 2 4 subge0d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)↔{B}\mathrm{mod}{C}\le {A}\mathrm{mod}{C}\right)$
6 resubcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}-{B}\in ℝ$
7 6 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}-{B}\in ℝ$
8 simp3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in {ℝ}^{+}$
9 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \frac{{A}}{{C}}\in ℝ$
10 9 flcld ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{C}}⌋\in ℤ$
11 10 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{C}}⌋\in ℤ$
12 rerpdivcl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \frac{{B}}{{C}}\in ℝ$
13 12 flcld ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℤ$
14 13 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℤ$
15 11 14 zsubcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\in ℤ$
16 modcyc2 ${⊢}\left({A}-{B}\in ℝ\wedge {C}\in {ℝ}^{+}\wedge ⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\in ℤ\right)\to \left({A}-{B}-{C}\left(⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\right)\right)\mathrm{mod}{C}=\left({A}-{B}\right)\mathrm{mod}{C}$
17 7 8 15 16 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}-{B}-{C}\left(⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\right)\right)\mathrm{mod}{C}=\left({A}-{B}\right)\mathrm{mod}{C}$
18 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
19 18 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\in ℂ$
20 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
21 20 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\in ℂ$
22 rpre ${⊢}{C}\in {ℝ}^{+}\to {C}\in ℝ$
23 22 adantl ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in ℝ$
24 refldivcl ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{C}}⌋\in ℝ$
25 23 24 remulcld ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{A}}{{C}}⌋\in ℝ$
26 25 recnd ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{A}}{{C}}⌋\in ℂ$
27 26 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{A}}{{C}}⌋\in ℂ$
28 22 adantl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in ℝ$
29 refldivcl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℝ$
30 28 29 remulcld ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{B}}{{C}}⌋\in ℝ$
31 30 recnd ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{B}}{{C}}⌋\in ℂ$
32 31 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}⌊\frac{{B}}{{C}}⌋\in ℂ$
33 19 21 27 32 sub4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}-{B}-\left({C}⌊\frac{{A}}{{C}}⌋-{C}⌊\frac{{B}}{{C}}⌋\right)={A}-{C}⌊\frac{{A}}{{C}}⌋-\left({B}-{C}⌊\frac{{B}}{{C}}⌋\right)$
34 22 3ad2ant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in ℝ$
35 34 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in ℂ$
36 24 recnd ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{C}}⌋\in ℂ$
37 36 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{C}}⌋\in ℂ$
38 29 recnd ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℂ$
39 38 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to ⌊\frac{{B}}{{C}}⌋\in ℂ$
40 35 37 39 subdid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\left(⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\right)={C}⌊\frac{{A}}{{C}}⌋-{C}⌊\frac{{B}}{{C}}⌋$
41 40 oveq2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}-{B}-{C}\left(⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\right)={A}-{B}-\left({C}⌊\frac{{A}}{{C}}⌋-{C}⌊\frac{{B}}{{C}}⌋\right)$
42 modval ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}={A}-{C}⌊\frac{{A}}{{C}}⌋$
43 42 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}={A}-{C}⌊\frac{{A}}{{C}}⌋$
44 modval ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}={B}-{C}⌊\frac{{B}}{{C}}⌋$
45 44 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}={B}-{C}⌊\frac{{B}}{{C}}⌋$
46 43 45 oveq12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)={A}-{C}⌊\frac{{A}}{{C}}⌋-\left({B}-{C}⌊\frac{{B}}{{C}}⌋\right)$
47 33 41 46 3eqtr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}-{B}-{C}\left(⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\right)=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)$
48 47 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}-{B}-{C}\left(⌊\frac{{A}}{{C}}⌋-⌊\frac{{B}}{{C}}⌋\right)\right)\mathrm{mod}{C}=\left(\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}$
49 17 48 eqtr3d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}-{B}\right)\mathrm{mod}{C}=\left(\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}$
50 49 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to \left({A}-{B}\right)\mathrm{mod}{C}=\left(\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}$
51 2 4 resubcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\in ℝ$
52 51 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\in ℝ$
53 simpl3 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to {C}\in {ℝ}^{+}$
54 simpr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)$
55 modge0 ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to 0\le {B}\mathrm{mod}{C}$
56 55 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to 0\le {B}\mathrm{mod}{C}$
57 2 4 subge02d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(0\le {B}\mathrm{mod}{C}↔\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\le {A}\mathrm{mod}{C}\right)$
58 56 57 mpbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\le {A}\mathrm{mod}{C}$
59 modlt ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}<{C}$
60 59 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}<{C}$
61 51 2 34 58 60 lelttrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)<{C}$
62 61 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)<{C}$
63 modid ${⊢}\left(\left(\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge \left(0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\wedge \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)<{C}\right)\right)\to \left(\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)$
64 52 53 54 62 63 syl22anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to \left(\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)$
65 50 64 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to \left({A}-{B}\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)$
66 modge0 ${⊢}\left({A}-{B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to 0\le \left({A}-{B}\right)\mathrm{mod}{C}$
67 6 66 stoic3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to 0\le \left({A}-{B}\right)\mathrm{mod}{C}$
68 67 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge \left({A}-{B}\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to 0\le \left({A}-{B}\right)\mathrm{mod}{C}$
69 simpr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge \left({A}-{B}\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to \left({A}-{B}\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)$
70 68 69 breqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge \left({A}-{B}\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)\to 0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)$
71 65 70 impbida ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(0\le \left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)↔\left({A}-{B}\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)$
72 5 71 bitr3d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{C}\le {A}\mathrm{mod}{C}↔\left({A}-{B}\right)\mathrm{mod}{C}=\left({A}\mathrm{mod}{C}\right)-\left({B}\mathrm{mod}{C}\right)\right)$