# Metamath Proof Explorer

## Theorem modmulnn

Description: Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by NM, 2-Jan-2009)

Ref Expression
Assertion modmulnn ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}⌊{A}⌋\mathrm{mod}{N}\cdot {M}\le ⌊{N}{A}⌋\mathrm{mod}{N}\cdot {M}$

### Proof

Step Hyp Ref Expression
1 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
2 reflcl ${⊢}{A}\in ℝ\to ⌊{A}⌋\in ℝ$
3 remulcl ${⊢}\left({N}\in ℝ\wedge ⌊{A}⌋\in ℝ\right)\to {N}⌊{A}⌋\in ℝ$
4 1 2 3 syl2an ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\right)\to {N}⌊{A}⌋\in ℝ$
5 4 3adant3 ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}⌊{A}⌋\in ℝ$
6 remulcl ${⊢}\left({N}\in ℝ\wedge {A}\in ℝ\right)\to {N}{A}\in ℝ$
7 1 6 sylan ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\right)\to {N}{A}\in ℝ$
8 reflcl ${⊢}{N}{A}\in ℝ\to ⌊{N}{A}⌋\in ℝ$
9 7 8 syl ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\right)\to ⌊{N}{A}⌋\in ℝ$
10 9 3adant3 ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊{N}{A}⌋\in ℝ$
11 nnmulcl ${⊢}\left({N}\in ℕ\wedge {M}\in ℕ\right)\to {N}\cdot {M}\in ℕ$
12 11 nnred ${⊢}\left({N}\in ℕ\wedge {M}\in ℕ\right)\to {N}\cdot {M}\in ℝ$
13 12 3adant2 ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}\cdot {M}\in ℝ$
14 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
15 nnne0 ${⊢}{N}\in ℕ\to {N}\ne 0$
16 14 15 jca ${⊢}{N}\in ℕ\to \left({N}\in ℂ\wedge {N}\ne 0\right)$
17 nncn ${⊢}{M}\in ℕ\to {M}\in ℂ$
18 nnne0 ${⊢}{M}\in ℕ\to {M}\ne 0$
19 17 18 jca ${⊢}{M}\in ℕ\to \left({M}\in ℂ\wedge {M}\ne 0\right)$
20 mulne0 ${⊢}\left(\left({N}\in ℂ\wedge {N}\ne 0\right)\wedge \left({M}\in ℂ\wedge {M}\ne 0\right)\right)\to {N}\cdot {M}\ne 0$
21 16 19 20 syl2an ${⊢}\left({N}\in ℕ\wedge {M}\in ℕ\right)\to {N}\cdot {M}\ne 0$
22 21 3adant2 ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}\cdot {M}\ne 0$
23 5 13 22 redivcld ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to \frac{{N}⌊{A}⌋}{{N}\cdot {M}}\in ℝ$
24 reflcl ${⊢}\frac{{N}⌊{A}⌋}{{N}\cdot {M}}\in ℝ\to ⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋\in ℝ$
25 23 24 syl ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋\in ℝ$
26 13 25 remulcld ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋\in ℝ$
27 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
28 flmulnn0 ${⊢}\left({N}\in {ℕ}_{0}\wedge {A}\in ℝ\right)\to {N}⌊{A}⌋\le ⌊{N}{A}⌋$
29 27 28 sylan ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\right)\to {N}⌊{A}⌋\le ⌊{N}{A}⌋$
30 29 3adant3 ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}⌊{A}⌋\le ⌊{N}{A}⌋$
31 5 10 26 30 lesub1dd ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}⌊{A}⌋-{N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋\le ⌊{N}{A}⌋-{N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
32 11 nnrpd ${⊢}\left({N}\in ℕ\wedge {M}\in ℕ\right)\to {N}\cdot {M}\in {ℝ}^{+}$
33 modval ${⊢}\left({N}⌊{A}⌋\in ℝ\wedge {N}\cdot {M}\in {ℝ}^{+}\right)\to {N}⌊{A}⌋\mathrm{mod}{N}\cdot {M}={N}⌊{A}⌋-{N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
34 5 32 33 3imp3i2an ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}⌊{A}⌋\mathrm{mod}{N}\cdot {M}={N}⌊{A}⌋-{N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
35 modval ${⊢}\left(⌊{N}{A}⌋\in ℝ\wedge {N}\cdot {M}\in {ℝ}^{+}\right)\to ⌊{N}{A}⌋\mathrm{mod}{N}\cdot {M}=⌊{N}{A}⌋-{N}\cdot {M}⌊\frac{⌊{N}{A}⌋}{{N}\cdot {M}}⌋$
36 10 32 35 3imp3i2an ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊{N}{A}⌋\mathrm{mod}{N}\cdot {M}=⌊{N}{A}⌋-{N}\cdot {M}⌊\frac{⌊{N}{A}⌋}{{N}\cdot {M}}⌋$
37 7 3adant3 ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}{A}\in ℝ$
38 fldiv ${⊢}\left({N}{A}\in ℝ\wedge {N}\cdot {M}\in ℕ\right)\to ⌊\frac{⌊{N}{A}⌋}{{N}\cdot {M}}⌋=⌊\frac{{N}{A}}{{N}\cdot {M}}⌋$
39 37 11 38 3imp3i2an ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊\frac{⌊{N}{A}⌋}{{N}\cdot {M}}⌋=⌊\frac{{N}{A}}{{N}\cdot {M}}⌋$
40 fldiv ${⊢}\left({A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊\frac{⌊{A}⌋}{{M}}⌋=⌊\frac{{A}}{{M}}⌋$
41 40 3adant3 ${⊢}\left({A}\in ℝ\wedge {M}\in ℕ\wedge {N}\in ℕ\right)\to ⌊\frac{⌊{A}⌋}{{M}}⌋=⌊\frac{{A}}{{M}}⌋$
42 2 recnd ${⊢}{A}\in ℝ\to ⌊{A}⌋\in ℂ$
43 divcan5 ${⊢}\left(⌊{A}⌋\in ℂ\wedge \left({M}\in ℂ\wedge {M}\ne 0\right)\wedge \left({N}\in ℂ\wedge {N}\ne 0\right)\right)\to \frac{{N}⌊{A}⌋}{{N}\cdot {M}}=\frac{⌊{A}⌋}{{M}}$
44 42 19 16 43 syl3an ${⊢}\left({A}\in ℝ\wedge {M}\in ℕ\wedge {N}\in ℕ\right)\to \frac{{N}⌊{A}⌋}{{N}\cdot {M}}=\frac{⌊{A}⌋}{{M}}$
45 44 fveq2d ${⊢}\left({A}\in ℝ\wedge {M}\in ℕ\wedge {N}\in ℕ\right)\to ⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋=⌊\frac{⌊{A}⌋}{{M}}⌋$
46 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
47 divcan5 ${⊢}\left({A}\in ℂ\wedge \left({M}\in ℂ\wedge {M}\ne 0\right)\wedge \left({N}\in ℂ\wedge {N}\ne 0\right)\right)\to \frac{{N}{A}}{{N}\cdot {M}}=\frac{{A}}{{M}}$
48 46 19 16 47 syl3an ${⊢}\left({A}\in ℝ\wedge {M}\in ℕ\wedge {N}\in ℕ\right)\to \frac{{N}{A}}{{N}\cdot {M}}=\frac{{A}}{{M}}$
49 48 fveq2d ${⊢}\left({A}\in ℝ\wedge {M}\in ℕ\wedge {N}\in ℕ\right)\to ⌊\frac{{N}{A}}{{N}\cdot {M}}⌋=⌊\frac{{A}}{{M}}⌋$
50 41 45 49 3eqtr4rd ${⊢}\left({A}\in ℝ\wedge {M}\in ℕ\wedge {N}\in ℕ\right)\to ⌊\frac{{N}{A}}{{N}\cdot {M}}⌋=⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
51 50 3comr ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊\frac{{N}{A}}{{N}\cdot {M}}⌋=⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
52 39 51 eqtrd ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊\frac{⌊{N}{A}⌋}{{N}\cdot {M}}⌋=⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
53 52 oveq2d ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}\cdot {M}⌊\frac{⌊{N}{A}⌋}{{N}\cdot {M}}⌋={N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
54 53 oveq2d ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊{N}{A}⌋-{N}\cdot {M}⌊\frac{⌊{N}{A}⌋}{{N}\cdot {M}}⌋=⌊{N}{A}⌋-{N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
55 36 54 eqtrd ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to ⌊{N}{A}⌋\mathrm{mod}{N}\cdot {M}=⌊{N}{A}⌋-{N}\cdot {M}⌊\frac{{N}⌊{A}⌋}{{N}\cdot {M}}⌋$
56 31 34 55 3brtr4d ${⊢}\left({N}\in ℕ\wedge {A}\in ℝ\wedge {M}\in ℕ\right)\to {N}⌊{A}⌋\mathrm{mod}{N}\cdot {M}\le ⌊{N}{A}⌋\mathrm{mod}{N}\cdot {M}$