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

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	|- I = ( 0 ..^ N )
2		eluz5nn	|- ( N e. ( ZZ>= ` 5 ) -> N e. NN )
3	2	adantr	|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> N e. NN )
4		simpr	|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> Y e. I )
5		2z	|- 2 e. ZZ
6	5	a1i	|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 2 e. ZZ )
7		1zzd	|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 1 e. ZZ )
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	|- ( N e. ( ZZ>= ` 5 ) <-> ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) )
13		1red	|- ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 1 e. RR )
14		5re	|- 5 e. RR
15	14	a1i	|- ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 5 e. RR )
16		zre	|- ( N e. ZZ -> N e. RR )
17	16	3ad2ant2	|- ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> N e. RR )
18		1lt5	|- 1 < 5
19	18	a1i	|- ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 1 < 5 )
20		simp3	|- ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 5 <_ N )
21	13 15 17 19 20	ltletrd	|- ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 1 < N )
22	12 21	sylbi	|- ( N e. ( ZZ>= ` 5 ) -> 1 < N )
23		1elfzo1	|- ( 1 e. ( 1 ..^ N ) <-> ( N e. NN /\ 1 < N ) )
24	2 22 23	sylanbrc	|- ( N e. ( ZZ>= ` 5 ) -> 1 e. ( 1 ..^ N ) )
25	24	adantr	|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 1 e. ( 1 ..^ N ) )
26	11 25	eqeltrid	|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( abs ` ( 2 - 1 ) ) e. ( 1 ..^ N ) )
27	1	mod2addne	|- ( ( N e. NN /\ ( Y e. I /\ 2 e. ZZ /\ 1 e. ZZ ) /\ ( abs ` ( 2 - 1 ) ) e. ( 1 ..^ N ) ) -> ( ( Y + 2 ) mod N ) =/= ( ( Y + 1 ) mod N ) )
28	3 4 6 7 26 27	syl131anc	|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y + 2 ) mod N ) =/= ( ( Y + 1 ) mod N ) )