This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 · 𝑀 ) ) )