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

Metamath Proof Explorer

Theorem modmulnn

Proof