Theorem modp2nep1

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

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

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		eluz5nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 𝑁 ∈ ℕ )
3	2	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 𝑁 ∈ ℕ )
4		simpr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐼 )
5		2z	⊢ 2 ∈ ℤ
6	5	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 2 ∈ ℤ )
7		1zzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 1 ∈ ℤ )
8		2m1e1	⊢ ( 2 − 1 ) = 1
9	8	fveq2i	⊢ ( abs ‘ ( 2 − 1 ) ) = ( abs ‘ 1 )
10		abs1	⊢ ( abs ‘ 1 ) = 1
11	9 10	eqtri	⊢ ( abs ‘ ( 2 − 1 ) ) = 1
12		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ↔ ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) )
13		1red	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 1 ∈ ℝ )
14		5re	⊢ 5 ∈ ℝ
15	14	a1i	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 5 ∈ ℝ )
16		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
17	16	3ad2ant2	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
18		1lt5	⊢ 1 < 5
19	18	a1i	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 1 < 5 )
20		simp3	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 5 ≤ 𝑁 )
21	13 15 17 19 20	ltletrd	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 1 < 𝑁 )
22	12 21	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 1 < 𝑁 )
23		1elfzo1	⊢ ( 1 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
24	2 22 23	sylanbrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 1 ∈ ( 1 ..^ 𝑁 ) )
25	24	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → 1 ∈ ( 1 ..^ 𝑁 ) )
26	11 25	eqeltrid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → ( abs ‘ ( 2 − 1 ) ) ∈ ( 1 ..^ 𝑁 ) )
27	1	mod2addne	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑌 ∈ 𝐼 ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( abs ‘ ( 2 − 1 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑌 + 2 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) )
28	3 4 6 7 26 27	syl131anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑌 ∈ 𝐼 ) → ( ( 𝑌 + 2 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) )