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	|- I = ( 0 ..^ N )
Assertion	modm1nep1	|- ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I ) -> ( ( Y - 1 ) mod N ) =/= ( ( Y + 1 ) mod N ) )

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	|- I = ( 0 ..^ N )
2		1elfzo1ceilhalf1	|- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
3	2	adantr	|- ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
4		eqid	|- ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
5	4 1	modmknepk	|- ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( Y - 1 ) mod N ) =/= ( ( Y + 1 ) mod N ) )
6	3 5	mpd3an3	|- ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I ) -> ( ( Y - 1 ) mod N ) =/= ( ( Y + 1 ) mod N ) )