modaddmodlo

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

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

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	$⊢ B \in (0 ..^M - (A \mod M)) \to B \in ℤ$
2	1	zred	$⊢ B \in (0 ..^M - (A \mod M)) \to B \in ℝ$
3	2	adantr	$⊢ (B \in (0 ..^M - (A \mod 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 (0 ..^M - (A \mod M)) \land (A \in ℤ \land M \in ℕ)) \to A \mod M \in ℝ$
7	3 6	readdcld	$⊢ (B \in (0 ..^M - (A \mod M)) \land (A \in ℤ \land M \in ℕ)) \to B + (A \mod M) \in ℝ$
8	7	ancoms	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod 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 (0 ..^M - (A \mod M))) \to M \in ℝ^{+}$
11	2	adantl	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to B \in ℝ$
12	5	adantr	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to A \mod M \in ℝ$
13		elfzole1	$⊢ B \in (0 ..^M - (A \mod M)) \to 0 \leq B$
14	13	adantl	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to 0 \leq B$
15	4	nn0ge0d	$⊢ (A \in ℤ \land M \in ℕ) \to 0 \leq A \mod M$
16	15	adantr	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to 0 \leq A \mod M$
17	11 12 14 16	addge0d	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to 0 \leq B + (A \mod M)$
18		elfzolt2	$⊢ B \in (0 ..^M - (A \mod M)) \to B < M - (A \mod M)$
19	18	adantl	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to B < M - (A \mod M)$
20		nnre	$⊢ M \in ℕ \to M \in ℝ$
21	20	ad2antlr	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to M \in ℝ$
22	11 12 21	ltaddsubd	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to (B + (A \mod M) < M \leftrightarrow B < M - (A \mod M))$
23	19 22	mpbird	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to B + (A \mod M) < M$
24		modid	$⊢ ((B + (A \mod M) \in ℝ \land M \in ℝ^{+}) \land (0 \leq B + (A \mod M) \land B + (A \mod M) < M)) \to (B + (A \mod M)) \mod M = B + (A \mod M)$
25	8 10 17 23 24	syl22anc	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to (B + (A \mod M)) \mod M = B + (A \mod M)$
26		zre	$⊢ A \in ℤ \to A \in ℝ$
27	26	adantr	$⊢ (A \in ℤ \land M \in ℕ) \to A \in ℝ$
28	27	adantr	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to A \in ℝ$
29		modadd2mod	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (B + (A \mod M)) \mod M = (B + A) \mod M$
30	28 11 10 29	syl3anc	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to (B + (A \mod M)) \mod M = (B + A) \mod M$
31	25 30	eqtr3d	$⊢ ((A \in ℤ \land M \in ℕ) \land B \in (0 ..^M - (A \mod M))) \to B + (A \mod M) = (B + A) \mod M$
32	31	ex	$⊢ (A \in ℤ \land M \in ℕ) \to (B \in (0 ..^M - (A \mod M)) \to B + (A \mod M) = (B + A) \mod M)$

Metamath Proof Explorer

Theorem modaddmodlo

Proof