modltm1p1mod

Description: If a real number modulo a positive real number is less than the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals the real number modulo the positive real number increased by 1. (Contributed by AV, 2-Nov-2018)

		Ref	Expression
	Assertion	modltm1p1mod	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to (A + 1) \mod M = (A \mod M) + 1$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \in ℝ$
2		1red	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to 1 \in ℝ$
3		simpr	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to M \in ℝ^{+}$
4	1 2 3	3jca	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \in ℝ \land 1 \in ℝ \land M \in ℝ^{+})$
5	4	3adant3	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to (A \in ℝ \land 1 \in ℝ \land M \in ℝ^{+})$
6		modaddmod	$⊢ (A \in ℝ \land 1 \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + 1) \mod M = (A + 1) \mod M$
7	5 6	syl	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to ((A \mod M) + 1) \mod M = (A + 1) \mod M$
8		modcl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℝ$
9		peano2re	$⊢ A \mod M \in ℝ \to (A \mod M) + 1 \in ℝ$
10	8 9	syl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M) + 1 \in ℝ$
11	10 3	jca	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + 1 \in ℝ \land M \in ℝ^{+})$
12	11	3adant3	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to ((A \mod M) + 1 \in ℝ \land M \in ℝ^{+})$
13		0red	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to 0 \in ℝ$
14		modge0	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to 0 \leq A \mod M$
15	8	lep1d	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \leq (A \mod M) + 1$
16	13 8 10 14 15	letrd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to 0 \leq (A \mod M) + 1$
17	16	3adant3	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to 0 \leq (A \mod M) + 1$
18		rpre	$⊢ M \in ℝ^{+} \to M \in ℝ$
19	18	adantl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to M \in ℝ$
20	8 2 19	ltaddsubd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + 1 < M \leftrightarrow A \mod M < M - 1)$
21	20	biimp3ar	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to (A \mod M) + 1 < M$
22		modid	$⊢ (((A \mod M) + 1 \in ℝ \land M \in ℝ^{+}) \land (0 \leq (A \mod M) + 1 \land (A \mod M) + 1 < M)) \to ((A \mod M) + 1) \mod M = (A \mod M) + 1$
23	12 17 21 22	syl12anc	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to ((A \mod M) + 1) \mod M = (A \mod M) + 1$
24	7 23	eqtr3d	$⊢ (A \in ℝ \land M \in ℝ^{+} \land A \mod M < M - 1) \to (A + 1) \mod M = (A \mod M) + 1$

Metamath Proof Explorer

Theorem modltm1p1mod

Proof