difmodm1lt

Description: The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd A and N = 2 , since ( ( A mod N ) - ( ( A - 1 ) mod N ) ) would be ( 1 - 0 ) = 1 which is not less than ( N - 1 ) = 1 . (Contributed by AV, 6-Jun-2012) (Proof shortened by SN, 27-Nov-2025)

		Ref	Expression
	Assertion	difmodm1lt	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N) - ((A - 1) \mod N) < N - 1$

Proof

Step	Hyp	Ref	Expression
1		peano2zm	$⊢ A \in ℤ \to A - 1 \in ℤ$
2	1	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A - 1 \in ℤ$
3	2	zred	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A - 1 \in ℝ$
4		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
5	4	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to N \in ℝ^{+}$
6	3 5	modcld	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A - 1) \mod N \in ℝ$
7	6	recnd	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A - 1) \mod N \in ℂ$
8		zre	$⊢ A \in ℤ \to A \in ℝ$
9	8	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A \in ℝ$
10	9 5	modcld	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A \mod N \in ℝ$
11	10	recnd	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to A \mod N \in ℂ$
12	7 11	negsubdi2d	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to - (((A - 1) \mod N) - (A \mod N)) = (A \mod N) - ((A - 1) \mod N)$
13		m1modmmod	$⊢ (A \in ℤ \land N \in ℕ) \to ((A - 1) \mod N) - (A \mod N) = if (A \mod N = 0, N - 1, - 1)$
14	13	3adant3	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to ((A - 1) \mod N) - (A \mod N) = if (A \mod N = 0, N - 1, - 1)$
15	14	negeqd	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to - (((A - 1) \mod N) - (A \mod N)) = - if (A \mod N = 0, N - 1, - 1)$
16	12 15	eqtr3d	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N) - ((A - 1) \mod N) = - if (A \mod N = 0, N - 1, - 1)$
17		iftrue	$⊢ A \mod N = 0 \to if (A \mod N = 0, N - 1, - 1) = N - 1$
18	17	adantr	$⊢ (A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to if (A \mod N = 0, N - 1, - 1) = N - 1$
19	18	negeqd	$⊢ (A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to - if (A \mod N = 0, N - 1, - 1) = - (N - 1)$
20		1red	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 1 \in ℝ$
21		2re	$⊢ 2 \in ℝ$
22	21	a1i	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 2 \in ℝ$
23		nnre	$⊢ N \in ℕ \to N \in ℝ$
24	23	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to N \in ℝ$
25		1lt2	$⊢ 1 < 2$
26	25	a1i	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 1 < 2$
27		simp3	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 2 < N$
28	20 22 24 26 27	lttrd	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 1 < N$
29		difrp	$⊢ (1 \in ℝ \land N \in ℝ) \to (1 < N \leftrightarrow N - 1 \in ℝ^{+})$
30	20 24 29	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (1 < N \leftrightarrow N - 1 \in ℝ^{+})$
31	28 30	mpbid	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to N - 1 \in ℝ^{+}$
32		neglt	$⊢ N - 1 \in ℝ^{+} \to - (N - 1) < N - 1$
33	31 32	syl	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to - (N - 1) < N - 1$
34	33	adantl	$⊢ (A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to - (N - 1) < N - 1$
35	19 34	eqbrtrd	$⊢ (A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to - if (A \mod N = 0, N - 1, - 1) < N - 1$
36		iffalse	$⊢ \neg A \mod N = 0 \to if (A \mod N = 0, N - 1, - 1) = - 1$
37	36	adantr	$⊢ (\neg A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to if (A \mod N = 0, N - 1, - 1) = - 1$
38	37	negeqd	$⊢ (\neg A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to - if (A \mod N = 0, N - 1, - 1) = - -1$
39		negneg1e1	$⊢ - -1 = 1$
40		df-2	$⊢ 2 = 1 + 1$
41	40	breq1i	$⊢ 2 < N \leftrightarrow 1 + 1 < N$
42	41	biimpi	$⊢ 2 < N \to 1 + 1 < N$
43	42	3ad2ant3	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 1 + 1 < N$
44	20 20 24	ltaddsub2d	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (1 + 1 < N \leftrightarrow 1 < N - 1)$
45	43 44	mpbid	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to 1 < N - 1$
46	39 45	eqbrtrid	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to - -1 < N - 1$
47	46	adantl	$⊢ (\neg A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to - -1 < N - 1$
48	38 47	eqbrtrd	$⊢ (\neg A \mod N = 0 \land (A \in ℤ \land N \in ℕ \land 2 < N)) \to - if (A \mod N = 0, N - 1, - 1) < N - 1$
49	35 48	pm2.61ian	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to - if (A \mod N = 0, N - 1, - 1) < N - 1$
50	16 49	eqbrtrd	$⊢ (A \in ℤ \land N \in ℕ \land 2 < N) \to (A \mod N) - ((A - 1) \mod N) < N - 1$

Metamath Proof Explorer

Theorem difmodm1lt

Proof