modsubdir

Description: Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008)

		Ref	Expression
	Assertion	modsubdir	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (B \mod C \leq A \mod C \leftrightarrow (A - B) \mod C = (A \mod C) - (B \mod C))$

Proof

Step	Hyp	Ref	Expression
1		modcl	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to A \mod C \in ℝ$
2	1	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A \mod C \in ℝ$
3		modcl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to B \mod C \in ℝ$
4	3	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to B \mod C \in ℝ$
5	2 4	subge0d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (0 \leq (A \mod C) - (B \mod C) \leftrightarrow B \mod C \leq A \mod C)$
6		resubcl	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℝ$
7	6	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A - B \in ℝ$
8		simp3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to C \in ℝ^{+}$
9		rerpdivcl	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to \frac{A}{C} \in ℝ$
10	9	flcld	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{A}{C}⌋ \in ℤ$
11	10	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{A}{C}⌋ \in ℤ$
12		rerpdivcl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to \frac{B}{C} \in ℝ$
13	12	flcld	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℤ$
14	13	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℤ$
15	11 14	zsubcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋ \in ℤ$
16		modcyc2	$⊢ (A - B \in ℝ \land C \in ℝ^{+} \land ⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋ \in ℤ) \to (A - B - C (⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋)) \mod C = (A - B) \mod C$
17	7 8 15 16	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A - B - C (⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋)) \mod C = (A - B) \mod C$
18		recn	$⊢ A \in ℝ \to A \in ℂ$
19	18	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A \in ℂ$
20		recn	$⊢ B \in ℝ \to B \in ℂ$
21	20	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to B \in ℂ$
22		rpre	$⊢ C \in ℝ^{+} \to C \in ℝ$
23	22	adantl	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to C \in ℝ$
24		refldivcl	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{A}{C}⌋ \in ℝ$
25	23 24	remulcld	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{A}{C}⌋ \in ℝ$
26	25	recnd	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{A}{C}⌋ \in ℂ$
27	26	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{A}{C}⌋ \in ℂ$
28	22	adantl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to C \in ℝ$
29		refldivcl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℝ$
30	28 29	remulcld	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{B}{C}⌋ \in ℝ$
31	30	recnd	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{B}{C}⌋ \in ℂ$
32	31	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{B}{C}⌋ \in ℂ$
33	19 21 27 32	sub4d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A - B - (C ⌊\frac{A}{C}⌋ - C ⌊\frac{B}{C}⌋) = A - C ⌊\frac{A}{C}⌋ - (B - C ⌊\frac{B}{C}⌋)$
34	22	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to C \in ℝ$
35	34	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to C \in ℂ$
36	24	recnd	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{A}{C}⌋ \in ℂ$
37	36	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{A}{C}⌋ \in ℂ$
38	29	recnd	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℂ$
39	38	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℂ$
40	35 37 39	subdid	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to C (⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋) = C ⌊\frac{A}{C}⌋ - C ⌊\frac{B}{C}⌋$
41	40	oveq2d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A - B - C (⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋) = A - B - (C ⌊\frac{A}{C}⌋ - C ⌊\frac{B}{C}⌋)$
42		modval	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to A \mod C = A - C ⌊\frac{A}{C}⌋$
43	42	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A \mod C = A - C ⌊\frac{A}{C}⌋$
44		modval	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to B \mod C = B - C ⌊\frac{B}{C}⌋$
45	44	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to B \mod C = B - C ⌊\frac{B}{C}⌋$
46	43 45	oveq12d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C) - (B \mod C) = A - C ⌊\frac{A}{C}⌋ - (B - C ⌊\frac{B}{C}⌋)$
47	33 41 46	3eqtr4d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A - B - C (⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋) = (A \mod C) - (B \mod C)$
48	47	oveq1d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A - B - C (⌊\frac{A}{C}⌋ - ⌊\frac{B}{C}⌋)) \mod C = ((A \mod C) - (B \mod C)) \mod C$
49	17 48	eqtr3d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A - B) \mod C = ((A \mod C) - (B \mod C)) \mod C$
50	49	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land 0 \leq (A \mod C) - (B \mod C)) \to (A - B) \mod C = ((A \mod C) - (B \mod C)) \mod C$
51	2 4	resubcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C) - (B \mod C) \in ℝ$
52	51	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land 0 \leq (A \mod C) - (B \mod C)) \to (A \mod C) - (B \mod C) \in ℝ$
53		simpl3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land 0 \leq (A \mod C) - (B \mod C)) \to C \in ℝ^{+}$
54		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land 0 \leq (A \mod C) - (B \mod C)) \to 0 \leq (A \mod C) - (B \mod C)$
55		modge0	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to 0 \leq B \mod C$
56	55	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to 0 \leq B \mod C$
57	2 4	subge02d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (0 \leq B \mod C \leftrightarrow (A \mod C) - (B \mod C) \leq A \mod C)$
58	56 57	mpbid	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C) - (B \mod C) \leq A \mod C$
59		modlt	$⊢ (A \in ℝ \land C \in ℝ^{+}) \to A \mod C < C$
60	59	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to A \mod C < C$
61	51 2 34 58 60	lelttrd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (A \mod C) - (B \mod C) < C$
62	61	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land 0 \leq (A \mod C) - (B \mod C)) \to (A \mod C) - (B \mod C) < C$
63		modid	$⊢ (((A \mod C) - (B \mod C) \in ℝ \land C \in ℝ^{+}) \land (0 \leq (A \mod C) - (B \mod C) \land (A \mod C) - (B \mod C) < C)) \to ((A \mod C) - (B \mod C)) \mod C = (A \mod C) - (B \mod C)$
64	52 53 54 62 63	syl22anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land 0 \leq (A \mod C) - (B \mod C)) \to ((A \mod C) - (B \mod C)) \mod C = (A \mod C) - (B \mod C)$
65	50 64	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land 0 \leq (A \mod C) - (B \mod C)) \to (A - B) \mod C = (A \mod C) - (B \mod C)$
66		modge0	$⊢ (A - B \in ℝ \land C \in ℝ^{+}) \to 0 \leq (A - B) \mod C$
67	6 66	stoic3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to 0 \leq (A - B) \mod C$
68	67	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land (A - B) \mod C = (A \mod C) - (B \mod C)) \to 0 \leq (A - B) \mod C$
69		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land (A - B) \mod C = (A \mod C) - (B \mod C)) \to (A - B) \mod C = (A \mod C) - (B \mod C)$
70	68 69	breqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \land (A - B) \mod C = (A \mod C) - (B \mod C)) \to 0 \leq (A \mod C) - (B \mod C)$
71	65 70	impbida	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (0 \leq (A \mod C) - (B \mod C) \leftrightarrow (A - B) \mod C = (A \mod C) - (B \mod C))$
72	5 71	bitr3d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ^{+}) \to (B \mod C \leq A \mod C \leftrightarrow (A - B) \mod C = (A \mod C) - (B \mod C))$

Metamath Proof Explorer

Theorem modsubdir

Proof