Metamath Proof Explorer

Theorem modm1p1mod0

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

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

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		modaddmod	$⊢ (A \in ℝ \land 1 \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + 1) \mod M = (A + 1) \mod M$
3	1 2	mp3an2	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + 1) \mod M = (A + 1) \mod M$
4	3	eqcomd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A + 1) \mod M = ((A \mod M) + 1) \mod M$
5	4	adantr	$⊢ ((A \in ℝ \land M \in ℝ^{+}) \land A \mod M = M - 1) \to (A + 1) \mod M = ((A \mod M) + 1) \mod M$
6		oveq1	$⊢ A \mod M = M - 1 \to (A \mod M) + 1 = M - 1 + 1$
7	6	oveq1d	$⊢ A \mod M = M - 1 \to ((A \mod M) + 1) \mod M = (M - 1 + 1) \mod M$
8		rpcn	$⊢ M \in ℝ^{+} \to M \in ℂ$
9		npcan1	$⊢ M \in ℂ \to M - 1 + 1 = M$
10	8 9	syl	$⊢ M \in ℝ^{+} \to M - 1 + 1 = M$
11	10	oveq1d	$⊢ M \in ℝ^{+} \to (M - 1 + 1) \mod M = M \mod M$
12		modid0	$⊢ M \in ℝ^{+} \to M \mod M = 0$
13	11 12	eqtrd	$⊢ M \in ℝ^{+} \to (M - 1 + 1) \mod M = 0$
14	13	adantl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (M - 1 + 1) \mod M = 0$
15	7 14	sylan9eqr	$⊢ ((A \in ℝ \land M \in ℝ^{+}) \land A \mod M = M - 1) \to ((A \mod M) + 1) \mod M = 0$
16	5 15	eqtrd	$⊢ ((A \in ℝ \land M \in ℝ^{+}) \land A \mod M = M - 1) \to (A + 1) \mod M = 0$
17	16	ex	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M = M - 1 \to (A + 1) \mod M = 0)$