Theorem modm1nem2

Description: A nonnegative integer less than a modulus greater than 4 minus one/minus two are not equal modulo the modulus. (Contributed by AV, 22-Nov-2025)

	Ref	Expression
Hypothesis	modm1nep1.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	modm1nem2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 − 2 ) mod 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		eluz5nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 𝑁 ∈ ℕ )
3	2	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 𝑁 ∈ ℕ )
4		simpr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐼 )
5		1zzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 1 ∈ ℤ )
6	5	znegcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → - 1 ∈ ℤ )
7		2z	⊢ 2 ∈ ℤ
8	7	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 2 ∈ ℤ )
9	8	znegcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → - 2 ∈ ℤ )
10		ax-1cn	⊢ 1 ∈ ℂ
11		2cn	⊢ 2 ∈ ℂ
12		neg2sub	⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℂ ) → ( - 1 − - 2 ) = ( 2 − 1 ) )
13	10 11 12	mp2an	⊢ ( - 1 − - 2 ) = ( 2 − 1 )
14		2m1e1	⊢ ( 2 − 1 ) = 1
15	13 14	eqtri	⊢ ( - 1 − - 2 ) = 1
16	15	fveq2i	⊢ ( abs ‘ ( - 1 − - 2 ) ) = ( abs ‘ 1 )
17		abs1	⊢ ( abs ‘ 1 ) = 1
18	16 17	eqtri	⊢ ( abs ‘ ( - 1 − - 2 ) ) = 1
19		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ↔ ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) )
20		1red	⊢ ( ( 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 1 ∈ ℝ )
21		5re	⊢ 5 ∈ ℝ
22	21	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 5 ∈ ℝ )
23		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
24	23	adantr	⊢ ( ( 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
25		1lt5	⊢ 1 < 5
26	25	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 1 < 5 )
27		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 5 ≤ 𝑁 )
28	20 22 24 26 27	ltletrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 1 < 𝑁 )
29	28	3adant1	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 1 < 𝑁 )
30	19 29	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 1 < 𝑁 )
31		1elfzo1	⊢ ( 1 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
32	2 30 31	sylanbrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 1 ∈ ( 1 ..^ 𝑁 ) )
33	32	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 1 ∈ ( 1 ..^ 𝑁 ) )
34	18 33	eqeltrid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → ( abs ‘ ( - 1 − - 2 ) ) ∈ ( 1 ..^ 𝑁 ) )
35	1	mod2addne	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑌 ∈ 𝐼 ∧ - 1 ∈ ℤ ∧ - 2 ∈ ℤ ) ∧ ( abs ‘ ( - 1 − - 2 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑌 + - 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + - 2 ) mod 𝑁 ) )
36	3 4 6 9 34 35	syl131anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → ( ( 𝑌 + - 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + - 2 ) mod 𝑁 ) )
37		elfzoelz	⊢ ( 𝑌 ∈ ( 0 ..^ 𝑁 ) → 𝑌 ∈ ℤ )
38	37 1	eleq2s	⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ )
39	38	zcnd	⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ ℂ )
40		1cnd	⊢ ( 𝑌 ∈ 𝐼 → 1 ∈ ℂ )
41	39 40	negsubd	⊢ ( 𝑌 ∈ 𝐼 → ( 𝑌 + - 1 ) = ( 𝑌 − 1 ) )
42	41	eqcomd	⊢ ( 𝑌 ∈ 𝐼 → ( 𝑌 − 1 ) = ( 𝑌 + - 1 ) )
43	42	oveq1d	⊢ ( 𝑌 ∈ 𝐼 → ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑌 + - 1 ) mod 𝑁 ) )
44		2cnd	⊢ ( 𝑌 ∈ 𝐼 → 2 ∈ ℂ )
45	39 44	negsubd	⊢ ( 𝑌 ∈ 𝐼 → ( 𝑌 + - 2 ) = ( 𝑌 − 2 ) )
46	45	eqcomd	⊢ ( 𝑌 ∈ 𝐼 → ( 𝑌 − 2 ) = ( 𝑌 + - 2 ) )
47	46	oveq1d	⊢ ( 𝑌 ∈ 𝐼 → ( ( 𝑌 − 2 ) mod 𝑁 ) = ( ( 𝑌 + - 2 ) mod 𝑁 ) )
48	43 47	neeq12d	⊢ ( 𝑌 ∈ 𝐼 → ( ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 − 2 ) mod 𝑁 ) ↔ ( ( 𝑌 + - 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + - 2 ) mod 𝑁 ) ) )
49	48	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 − 2 ) mod 𝑁 ) ↔ ( ( 𝑌 + - 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + - 2 ) mod 𝑁 ) ) )
50	36 49	mpbird	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 − 2 ) mod 𝑁 ) )