modaddmodup

Description: The sum of an integer modulo a positive integer and another integer minus the positive integer equals the sum of the two integers modulo the positive integer if the other integer is in the upper part of the range between 0 and the positive integer. (Contributed by AV, 30-Oct-2018)

		Ref	Expression
	Assertion	modaddmodup	$⊢ (A \in ℤ \land M \in ℕ) \to (B \in (M - (A \mod M) ..^M) \to B + (A \mod M) - M = (B + A) \mod M)$

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	$⊢ B \in (M - (A \mod M) ..^M) \to B \in ℤ$
2	1	zred	$⊢ B \in (M - (A \mod M) ..^M) \to B \in ℝ$
3	2	adantr	$⊢ (B \in (M - (A \mod M) ..^M) \land (A \in ℤ \land M \in ℕ)) \to B \in ℝ$
4		zmodcl	$⊢ (A \in ℤ \land M \in ℕ) \to A \mod M \in ℕ_{0}$
5	4	nn0red	$⊢ (A \in ℤ \land M \in ℕ) \to A \mod M \in ℝ$
6	5	adantl	$⊢ (B \in (M - (A \mod M) ..^M) \land (A \in ℤ \land M \in ℕ)) \to A \mod M \in ℝ$
7	3 6	readdcld	$⊢ (B \in (M - (A \mod M) ..^M) \land (A \in ℤ \land M \in ℕ)) \to B + (A \mod M) \in ℝ$
8	7	ancoms	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to B + (A \mod M) \in ℝ$
9		nnrp	$⊢ M \in ℕ \to M \in ℝ^{+}$
10	9	ad2antlr	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to M \in ℝ^{+}$
11		elfzo2	$⊢ B \in (M - (A \mod M) ..^M) \leftrightarrow (B \in ℤ_{\geq (M - (A \mod M))} \land M \in ℤ \land B < M)$
12		eluz2	$⊢ B \in ℤ_{\geq (M - (A \mod M))} \leftrightarrow (M - (A \mod M) \in ℤ \land B \in ℤ \land M - (A \mod M) \leq B)$
13		nnre	$⊢ M \in ℕ \to M \in ℝ$
14	13	adantl	$⊢ (A \in ℤ \land M \in ℕ) \to M \in ℝ$
15	14	adantl	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to M \in ℝ$
16	5	adantl	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to A \mod M \in ℝ$
17		zre	$⊢ B \in ℤ \to B \in ℝ$
18	17	adantr	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to B \in ℝ$
19	15 16 18	lesubaddd	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to (M - (A \mod M) \leq B \leftrightarrow M \leq B + (A \mod M))$
20	19	biimpd	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to (M - (A \mod M) \leq B \to M \leq B + (A \mod M))$
21	20	impancom	$⊢ (B \in ℤ \land M - (A \mod M) \leq B) \to ((A \in ℤ \land M \in ℕ) \to M \leq B + (A \mod M))$
22	21	3adant1	$⊢ (M - (A \mod M) \in ℤ \land B \in ℤ \land M - (A \mod M) \leq B) \to ((A \in ℤ \land M \in ℕ) \to M \leq B + (A \mod M))$
23	12 22	sylbi	$⊢ B \in ℤ_{\geq (M - (A \mod M))} \to ((A \in ℤ \land M \in ℕ) \to M \leq B + (A \mod M))$
24	23	3ad2ant1	$⊢ (B \in ℤ_{\geq (M - (A \mod M))} \land M \in ℤ \land B < M) \to ((A \in ℤ \land M \in ℕ) \to M \leq B + (A \mod M))$
25	11 24	sylbi	$⊢ B \in (M - (A \mod M) ..^M) \to ((A \in ℤ \land M \in ℕ) \to M \leq B + (A \mod M))$
26	25	impcom	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to M \leq B + (A \mod M)$
27		eluzelz	$⊢ B \in ℤ_{\geq (M - (A \mod M))} \to B \in ℤ$
28	17 5	anim12i	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to (B \in ℝ \land A \mod M \in ℝ)$
29	13 13	jca	$⊢ M \in ℕ \to (M \in ℝ \land M \in ℝ)$
30	29	adantl	$⊢ (A \in ℤ \land M \in ℕ) \to (M \in ℝ \land M \in ℝ)$
31	30	adantl	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to (M \in ℝ \land M \in ℝ)$
32	28 31	jca	$⊢ (B \in ℤ \land (A \in ℤ \land M \in ℕ)) \to ((B \in ℝ \land A \mod M \in ℝ) \land (M \in ℝ \land M \in ℝ))$
33	32	adantr	$⊢ ((B \in ℤ \land (A \in ℤ \land M \in ℕ)) \land B < M) \to ((B \in ℝ \land A \mod M \in ℝ) \land (M \in ℝ \land M \in ℝ))$
34		simpr	$⊢ ((B \in ℤ \land (A \in ℤ \land M \in ℕ)) \land B < M) \to B < M$
35		zre	$⊢ A \in ℤ \to A \in ℝ$
36		modlt	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M < M$
37	35 9 36	syl2an	$⊢ (A \in ℤ \land M \in ℕ) \to A \mod M < M$
38	5 14 37	ltled	$⊢ (A \in ℤ \land M \in ℕ) \to A \mod M \leq M$
39	38	ad2antlr	$⊢ ((B \in ℤ \land (A \in ℤ \land M \in ℕ)) \land B < M) \to A \mod M \leq M$
40	34 39	jca	$⊢ ((B \in ℤ \land (A \in ℤ \land M \in ℕ)) \land B < M) \to (B < M \land A \mod M \leq M)$
41		ltleadd	$⊢ ((B \in ℝ \land A \mod M \in ℝ) \land (M \in ℝ \land M \in ℝ)) \to ((B < M \land A \mod M \leq M) \to B + (A \mod M) < M + M)$
42	33 40 41	sylc	$⊢ ((B \in ℤ \land (A \in ℤ \land M \in ℕ)) \land B < M) \to B + (A \mod M) < M + M$
43		nncn	$⊢ M \in ℕ \to M \in ℂ$
44	43	2timesd	$⊢ M \in ℕ \to 2 \cdot M = M + M$
45	44	adantl	$⊢ (A \in ℤ \land M \in ℕ) \to 2 \cdot M = M + M$
46	45	ad2antlr	$⊢ ((B \in ℤ \land (A \in ℤ \land M \in ℕ)) \land B < M) \to 2 \cdot M = M + M$
47	42 46	breqtrrd	$⊢ ((B \in ℤ \land (A \in ℤ \land M \in ℕ)) \land B < M) \to B + (A \mod M) < 2 \cdot M$
48	47	exp31	$⊢ B \in ℤ \to ((A \in ℤ \land M \in ℕ) \to (B < M \to B + (A \mod M) < 2 \cdot M))$
49	48	com23	$⊢ B \in ℤ \to (B < M \to ((A \in ℤ \land M \in ℕ) \to B + (A \mod M) < 2 \cdot M))$
50	27 49	syl	$⊢ B \in ℤ_{\geq (M - (A \mod M))} \to (B < M \to ((A \in ℤ \land M \in ℕ) \to B + (A \mod M) < 2 \cdot M))$
51	50	imp	$⊢ (B \in ℤ_{\geq (M - (A \mod M))} \land B < M) \to ((A \in ℤ \land M \in ℕ) \to B + (A \mod M) < 2 \cdot M)$
52	51	3adant2	$⊢ (B \in ℤ_{\geq (M - (A \mod M))} \land M \in ℤ \land B < M) \to ((A \in ℤ \land M \in ℕ) \to B + (A \mod M) < 2 \cdot M)$
53	11 52	sylbi	$⊢ B \in (M - (A \mod M) ..^M) \to ((A \in ℤ \land M \in ℕ) \to B + (A \mod M) < 2 \cdot M)$
54	53	impcom	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to B + (A \mod M) < 2 \cdot M$
55		2submod	$⊢ ((B + (A \mod M) \in ℝ \land M \in ℝ^{+}) \land (M \leq B + (A \mod M) \land B + (A \mod M) < 2 \cdot M)) \to (B + (A \mod M)) \mod M = B + (A \mod M) - M$
56	55	eqcomd	$⊢ ((B + (A \mod M) \in ℝ \land M \in ℝ^{+}) \land (M \leq B + (A \mod M) \land B + (A \mod M) < 2 \cdot M)) \to B + (A \mod M) - M = (B + (A \mod M)) \mod M$
57	8 10 26 54 56	syl22anc	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to B + (A \mod M) - M = (B + (A \mod M)) \mod M$
58	35	adantr	$⊢ (A \in ℤ \land M \in ℕ) \to A \in ℝ$
59	58	adantr	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to A \in ℝ$
60	2	adantl	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to B \in ℝ$
61		modadd2mod	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (B + (A \mod M)) \mod M = (B + A) \mod M$
62	59 60 10 61	syl3anc	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to (B + (A \mod M)) \mod M = (B + A) \mod M$
63	57 62	eqtrd	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (M - (A \mod M) ..^M)) \to B + (A \mod M) - M = (B + A) \mod M$
64	63	ex	$⊢ (A \in ℤ \land M \in ℕ) \to (B \in (M - (A \mod M) ..^M) \to B + (A \mod M) - M = (B + A) \mod M)$

Metamath Proof Explorer

Theorem modaddmodup

Proof