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