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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) ≤ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
2 reflcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
3 remulcl ( ( 𝑁 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
4 1 2 3 syl2an ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
5 4 3adant3 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
6 remulcl ( ( 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · 𝐴 ) ∈ ℝ )
7 1 6 sylan ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · 𝐴 ) ∈ ℝ )
8 reflcl ( ( 𝑁 · 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ )
9 7 8 syl ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ )
10 9 3adant3 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ )
11 nnmulcl ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℕ )
12 11 nnred ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℝ )
13 12 3adant2 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℝ )
14 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
15 nnne0 ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
16 14 15 jca ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
17 nncn ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
18 nnne0 ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 )
19 17 18 jca ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
20 mulne0 ( ( ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ) → ( 𝑁 · 𝑀 ) ≠ 0 )
21 16 19 20 syl2an ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ≠ 0 )
22 21 3adant2 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ≠ 0 )
23 5 13 22 redivcld ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ∈ ℝ )
24 reflcl ( ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ∈ ℝ )
25 23 24 syl ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ∈ ℝ )
26 13 25 remulcld ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ∈ ℝ )
27 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
28 flmulnn0 ( ( 𝑁 ∈ ℕ0𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) )
29 27 28 sylan ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) )
30 29 3adant3 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) )
31 5 10 26 30 lesub1dd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ≤ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) )
32 11 nnrpd ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℝ+ )
33 modval ( ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝑁 · 𝑀 ) ∈ ℝ+ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) )
34 5 32 33 3imp3i2an ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) )
35 modval ( ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ ∧ ( 𝑁 · 𝑀 ) ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) )
36 10 32 35 3imp3i2an ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) )
37 7 3adant3 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝐴 ) ∈ ℝ )
38 fldiv ( ( ( 𝑁 · 𝐴 ) ∈ ℝ ∧ ( 𝑁 · 𝑀 ) ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) )
39 37 11 38 3imp3i2an ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) )
40 fldiv ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
41 40 3adant3 ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
42 2 recnd ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
43 divcan5 ( ( ( ⌊ ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) )
44 42 19 16 43 syl3an ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) )
45 44 fveq2d ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) )
46 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
47 divcan5 ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) = ( 𝐴 / 𝑀 ) )
48 46 19 16 47 syl3an ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) = ( 𝐴 / 𝑀 ) )
49 48 fveq2d ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
50 41 45 49 3eqtr4rd ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) )
51 50 3comr ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) )
52 39 51 eqtrd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) )
53 52 oveq2d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) = ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) )
54 53 oveq2d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) )
55 36 54 eqtrd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) )
56 31 34 55 3brtr4d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) ≤ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) )