Theorem modm1nep1

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

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

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		1elfzo1ceilhalf1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
3	2	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
4		eqid	⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
5	4 1	modmknepk	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) )
6	3 5	mpd3an3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ) → ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) )