modadd1

Description: Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008)

		Ref	Expression
	Assertion	modadd1	$⊢ ((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	syl6bi	$⊢ ((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		recn	$⊢ A \in ℝ \to A \in ℂ$
9	8	adantr	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to A \in ℂ$
10		recn	$⊢ C \in ℝ \to C \in ℂ$
11	10	ad2antrl	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to C \in ℂ$
12		rpcn	$⊢ D \in ℝ^{+} \to D \in ℂ$
13	12	adantl	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to D \in ℂ$
14		rerpdivcl	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to \frac{A}{D} \in ℝ$
15		reflcl	$⊢ \frac{A}{D} \in ℝ \to ⌊\frac{A}{D}⌋ \in ℝ$
16	15	recnd	$⊢ \frac{A}{D} \in ℝ \to ⌊\frac{A}{D}⌋ \in ℂ$
17	14 16	syl	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{A}{D}⌋ \in ℂ$
18	13 17	mulcld	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to D ⌊\frac{A}{D}⌋ \in ℂ$
19	18	adantrl	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to D ⌊\frac{A}{D}⌋ \in ℂ$
20	9 11 19	addsubd	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to A + C - D ⌊\frac{A}{D}⌋ = A - D ⌊\frac{A}{D}⌋ + C$
21	20	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A + C - D ⌊\frac{A}{D}⌋ = A - D ⌊\frac{A}{D}⌋ + C$
22		recn	$⊢ B \in ℝ \to B \in ℂ$
23	22	adantr	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to B \in ℂ$
24	10	ad2antrl	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to C \in ℂ$
25	12	adantl	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to D \in ℂ$
26		rerpdivcl	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to \frac{B}{D} \in ℝ$
27		reflcl	$⊢ \frac{B}{D} \in ℝ \to ⌊\frac{B}{D}⌋ \in ℝ$
28	27	recnd	$⊢ \frac{B}{D} \in ℝ \to ⌊\frac{B}{D}⌋ \in ℂ$
29	26 28	syl	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{B}{D}⌋ \in ℂ$
30	25 29	mulcld	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to D ⌊\frac{B}{D}⌋ \in ℂ$
31	30	adantrl	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to D ⌊\frac{B}{D}⌋ \in ℂ$
32	23 24 31	addsubd	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to B + C - D ⌊\frac{B}{D}⌋ = B - D ⌊\frac{B}{D}⌋ + C$
33	32	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B + C - D ⌊\frac{B}{D}⌋ = B - D ⌊\frac{B}{D}⌋ + C$
34	21 33	eqeq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A + C - D ⌊\frac{A}{D}⌋ = B + C - D ⌊\frac{B}{D}⌋ \leftrightarrow A - D ⌊\frac{A}{D}⌋ + C = B - D ⌊\frac{B}{D}⌋ + C)$
35	7 34	sylibrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \to A + C - D ⌊\frac{A}{D}⌋ = B + C - D ⌊\frac{B}{D}⌋)$
36		oveq1	$⊢ A + C - D ⌊\frac{A}{D}⌋ = B + C - D ⌊\frac{B}{D}⌋ \to (A + C - D ⌊\frac{A}{D}⌋) \mod D = (B + C - D ⌊\frac{B}{D}⌋) \mod D$
37		readdcl	$⊢ (A \in ℝ \land C \in ℝ) \to A + C \in ℝ$
38	37	adantrr	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to A + C \in ℝ$
39		simprr	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to D \in ℝ^{+}$
40	14	flcld	$⊢ (A \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{A}{D}⌋ \in ℤ$
41	40	adantrl	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to ⌊\frac{A}{D}⌋ \in ℤ$
42		modcyc2	$⊢ (A + C \in ℝ \land D \in ℝ^{+} \land ⌊\frac{A}{D}⌋ \in ℤ) \to (A + C - D ⌊\frac{A}{D}⌋) \mod D = (A + C) \mod D$
43	38 39 41 42	syl3anc	$⊢ (A \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to (A + C - D ⌊\frac{A}{D}⌋) \mod D = (A + C) \mod D$
44	43	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A + C - D ⌊\frac{A}{D}⌋) \mod D = (A + C) \mod D$
45		readdcl	$⊢ (B \in ℝ \land C \in ℝ) \to B + C \in ℝ$
46	45	adantrr	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to B + C \in ℝ$
47		simprr	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to D \in ℝ^{+}$
48	26	flcld	$⊢ (B \in ℝ \land D \in ℝ^{+}) \to ⌊\frac{B}{D}⌋ \in ℤ$
49	48	adantrl	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to ⌊\frac{B}{D}⌋ \in ℤ$
50		modcyc2	$⊢ (B + C \in ℝ \land D \in ℝ^{+} \land ⌊\frac{B}{D}⌋ \in ℤ) \to (B + C - D ⌊\frac{B}{D}⌋) \mod D = (B + C) \mod D$
51	46 47 49 50	syl3anc	$⊢ (B \in ℝ \land (C \in ℝ \land D \in ℝ^{+})) \to (B + C - D ⌊\frac{B}{D}⌋) \mod D = (B + C) \mod D$
52	51	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (B + C - D ⌊\frac{B}{D}⌋) \mod D = (B + C) \mod D$
53	44 52	eqeq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to ((A + C - D ⌊\frac{A}{D}⌋) \mod D = (B + C - D ⌊\frac{B}{D}⌋) \mod D \leftrightarrow (A + C) \mod D = (B + C) \mod D)$
54	36 53	imbitrid	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A + C - D ⌊\frac{A}{D}⌋ = B + C - D ⌊\frac{B}{D}⌋ \to (A + C) \mod D = (B + C) \mod D)$
55	35 54	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)$
56	55	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 modadd1

Proof