Theorem modm2nep1

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

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

Proof

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