modmul1

Description: Multiplication property of the modulo operation. Note that the multiplier C must be an integer. (Contributed by NM, 12-Nov-2008)

		Ref	Expression
	Assertion	modmul1	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+}) \land A \mod D = B \mod D) \to A C \mod D = B C \mod D$

Proof

Step	Hyp	Ref	Expression
1		modval	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to A \mod D = A - D ⌊\frac{A}{D}⌋$
2		modval	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to B \mod D = B - D ⌊\frac{B}{D}⌋$
3	1 2	eqeqan12d	$⊢ ((A \in ℝ \land D \in ℝ^{+}) \land (B \in ℝ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \leftrightarrow A - D ⌊\frac{A}{D}⌋ = B - D ⌊\frac{B}{D}⌋)$
4	3	anandirs	$⊢ ((A \in ℝ \land B \in ℝ) \land D \in ℝ^{+}) \to (A \mod D = B \mod D \leftrightarrow A - D ⌊\frac{A}{D}⌋ = B - D ⌊\frac{B}{D}⌋)$
5	4	adantrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \leftrightarrow A - D ⌊\frac{A}{D}⌋ = B - D ⌊\frac{B}{D}⌋)$
6		oveq1	$⊢ A - D ⌊\frac{A}{D}⌋ = B - D ⌊\frac{B}{D}⌋ \to (A - D ⌊\frac{A}{D}⌋) C = (B - D ⌊\frac{B}{D}⌋) C$
7	5 6	biimtrdi	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \to (A - D ⌊\frac{A}{D}⌋) C = (B - D ⌊\frac{B}{D}⌋) C)$
8		rpcn	$⊢ D \in ℝ^{+} \to D \in ℂ$
9	8	ad2antll	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D \in ℂ$
10		zcn	$⊢ C \in ℤ \to C \in ℂ$
11	10	ad2antrl	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to C \in ℂ$
12		rerpdivcl	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to \frac{A}{D} \in ℝ$
13	12	flcld	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{A}{D}⌋ \in ℤ$
14	13	zcnd	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{A}{D}⌋ \in ℂ$
15	14	adantrl	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to ⌊\frac{A}{D}⌋ \in ℂ$
16	9 11 15	mulassd	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D C ⌊\frac{A}{D}⌋ = D C ⌊\frac{A}{D}⌋$
17	9 11 15	mul32d	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D C ⌊\frac{A}{D}⌋ = D ⌊\frac{A}{D}⌋ C$
18	16 17	eqtr3d	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D C ⌊\frac{A}{D}⌋ = D ⌊\frac{A}{D}⌋ C$
19	18	oveq2d	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to A C - D C ⌊\frac{A}{D}⌋ = A C - D ⌊\frac{A}{D}⌋ C$
20		recn	$⊢ A \in ℝ \to A \in ℂ$
21	20	adantr	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to A \in ℂ$
22	8	adantl	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to D \in ℂ$
23	22 14	mulcld	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to D ⌊\frac{A}{D}⌋ \in ℂ$
24	23	adantrl	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D ⌊\frac{A}{D}⌋ \in ℂ$
25	21 24 11	subdird	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to (A - D ⌊\frac{A}{D}⌋) C = A C - D ⌊\frac{A}{D}⌋ C$
26	19 25	eqtr4d	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to A C - D C ⌊\frac{A}{D}⌋ = (A - D ⌊\frac{A}{D}⌋) C$
27	26	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to A C - D C ⌊\frac{A}{D}⌋ = (A - D ⌊\frac{A}{D}⌋) C$
28	8	ad2antll	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D \in ℂ$
29	10	ad2antrl	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to C \in ℂ$
30		rerpdivcl	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to \frac{B}{D} \in ℝ$
31	30	flcld	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{B}{D}⌋ \in ℤ$
32	31	zcnd	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{B}{D}⌋ \in ℂ$
33	32	adantrl	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to ⌊\frac{B}{D}⌋ \in ℂ$
34	28 29 33	mulassd	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D C ⌊\frac{B}{D}⌋ = D C ⌊\frac{B}{D}⌋$
35	28 29 33	mul32d	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D C ⌊\frac{B}{D}⌋ = D ⌊\frac{B}{D}⌋ C$
36	34 35	eqtr3d	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D C ⌊\frac{B}{D}⌋ = D ⌊\frac{B}{D}⌋ C$
37	36	oveq2d	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to B C - D C ⌊\frac{B}{D}⌋ = B C - D ⌊\frac{B}{D}⌋ C$
38		recn	$⊢ B \in ℝ \to B \in ℂ$
39	38	adantr	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to B \in ℂ$
40	8	adantl	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to D \in ℂ$
41	40 32	mulcld	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to D ⌊\frac{B}{D}⌋ \in ℂ$
42	41	adantrl	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D ⌊\frac{B}{D}⌋ \in ℂ$
43	39 42 29	subdird	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to (B - D ⌊\frac{B}{D}⌋) C = B C - D ⌊\frac{B}{D}⌋ C$
44	37 43	eqtr4d	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to B C - D C ⌊\frac{B}{D}⌋ = (B - D ⌊\frac{B}{D}⌋) C$
45	44	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to B C - D C ⌊\frac{B}{D}⌋ = (B - D ⌊\frac{B}{D}⌋) C$
46	27 45	eqeq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (A C - D C ⌊\frac{A}{D}⌋ = B C - D C ⌊\frac{B}{D}⌋ \leftrightarrow (A - D ⌊\frac{A}{D}⌋) C = (B - D ⌊\frac{B}{D}⌋) C)$
47	7 46	sylibrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \to A C - D C ⌊\frac{A}{D}⌋ = B C - D C ⌊\frac{B}{D}⌋)$
48		oveq1	$⊢ A C - D C ⌊\frac{A}{D}⌋ = B C - D C ⌊\frac{B}{D}⌋ \to (A C - D C ⌊\frac{A}{D}⌋) \mod D = (B C - D C ⌊\frac{B}{D}⌋) \mod D$
49		zre	$⊢ C \in ℤ \to C \in ℝ$
50		remulcl	$⊢ (A \in ℝ \land C \in ℝ) \to A C \in ℝ$
51	49 50	sylan2	$⊢ (A \in ℝ \land C \in ℤ) \to A C \in ℝ$
52	51	adantrr	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to A C \in ℝ$
53		simprr	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D \in ℝ^{+}$
54		simprl	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to C \in ℤ$
55	13	adantrl	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to ⌊\frac{A}{D}⌋ \in ℤ$
56	54 55	zmulcld	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to C ⌊\frac{A}{D}⌋ \in ℤ$
57		modcyc2	$⊢ (A C \in ℝ \land D \in ℝ^{+} \land C ⌊\frac{A}{D}⌋ \in ℤ) \to (A C - D C ⌊\frac{A}{D}⌋) \mod D = A C \mod D$
58	52 53 56 57	syl3anc	$⊢ (A \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to (A C - D C ⌊\frac{A}{D}⌋) \mod D = A C \mod D$
59	58	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (A C - D C ⌊\frac{A}{D}⌋) \mod D = A C \mod D$
60		remulcl	$⊢ (B \in ℝ \land C \in ℝ) \to B C \in ℝ$
61	49 60	sylan2	$⊢ (B \in ℝ \land C \in ℤ) \to B C \in ℝ$
62	61	adantrr	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to B C \in ℝ$
63		simprr	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to D \in ℝ^{+}$
64		simprl	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to C \in ℤ$
65	31	adantrl	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to ⌊\frac{B}{D}⌋ \in ℤ$
66	64 65	zmulcld	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to C ⌊\frac{B}{D}⌋ \in ℤ$
67		modcyc2	$⊢ (B C \in ℝ \land D \in ℝ^{+} \land C ⌊\frac{B}{D}⌋ \in ℤ) \to (B C - D C ⌊\frac{B}{D}⌋) \mod D = B C \mod D$
68	62 63 66 67	syl3anc	$⊢ (B \in ℝ \land (C \in ℤ \land D \in ℝ^{+})) \to (B C - D C ⌊\frac{B}{D}⌋) \mod D = B C \mod D$
69	68	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (B C - D C ⌊\frac{B}{D}⌋) \mod D = B C \mod D$
70	59 69	eqeq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to ((A C - D C ⌊\frac{A}{D}⌋) \mod D = (B C - D C ⌊\frac{B}{D}⌋) \mod D \leftrightarrow A C \mod D = B C \mod D)$
71	48 70	imbitrid	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (A C - D C ⌊\frac{A}{D}⌋ = B C - D C ⌊\frac{B}{D}⌋ \to A C \mod D = B C \mod D)$
72	47 71	syld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \to A C \mod D = B C \mod D)$
73	72	3impia	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℤ \land D \in ℝ^{+}) \land A \mod D = B \mod D) \to A C \mod D = B C \mod D$

Metamath Proof Explorer

Theorem modmul1

Proof