addmodid

Description: The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by Alexander van der Vekens, 30-Oct-2018) (Proof shortened by AV, 5-Jul-2020)

		Ref	Expression
	Assertion	addmodid	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (M + A) \mod M = A$

Proof

Step	Hyp	Ref	Expression
1		nncn	$⊢ M \in ℕ \to M \in ℂ$
2	1	mullidd	$⊢ M \in ℕ \to 1 \cdot M = M$
3	2	3ad2ant2	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to 1 \cdot M = M$
4	3	eqcomd	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to M = 1 \cdot M$
5	4	oveq1d	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to M + A = 1 \cdot M + A$
6	5	oveq1d	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (M + A) \mod M = (1 \cdot M + A) \mod M$
7		1zzd	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to 1 \in ℤ$
8		nnrp	$⊢ M \in ℕ \to M \in ℝ^{+}$
9	8	3ad2ant2	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to M \in ℝ^{+}$
10		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
11	10	rexrd	$⊢ A \in ℕ_{0} \to A \in ℝ^{*}$
12	11	3ad2ant1	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to A \in ℝ^{*}$
13		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
14	13	3ad2ant1	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to 0 \leq A$
15		simp3	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to A < M$
16		0xr	$⊢ 0 \in ℝ^{*}$
17		nnre	$⊢ M \in ℕ \to M \in ℝ$
18	17	rexrd	$⊢ M \in ℕ \to M \in ℝ^{*}$
19	18	3ad2ant2	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to M \in ℝ^{*}$
20		elico1	$⊢ (0 \in ℝ^{} \land M \in ℝ^{}) \to (A \in [0, M) \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A < M))$
21	16 19 20	sylancr	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (A \in [0, M) \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A < M))$
22	12 14 15 21	mpbir3and	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to A \in [0, M)$
23		muladdmodid	$⊢ (1 \in ℤ \land M \in ℝ^{+} \land A \in [0, M)) \to (1 \cdot M + A) \mod M = A$
24	7 9 22 23	syl3anc	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (1 \cdot M + A) \mod M = A$
25	6 24	eqtrd	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (M + A) \mod M = A$

Metamath Proof Explorer

Theorem addmodid

Proof