Metamath Proof Explorer

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 
|- I = ( 0 ..^ N )
Assertion modm2nep1 
|- ( ( 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 elfzoelz 
 |-  ( Y e. ( 0 ..^ N ) -> Y e. ZZ )
3 2 1 eleq2s 
 |-  ( Y e. I -> Y e. ZZ )
4 3 zcnd 
 |-  ( Y e. I -> Y e. CC )
5 2cnd 
 |-  ( Y e. I -> 2 e. CC )
6 4 5 negsubd 
 |-  ( Y e. I -> ( Y + -u 2 ) = ( Y - 2 ) )
7 6 adantl 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( Y + -u 2 ) = ( Y - 2 ) )
8 7 eqcomd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( Y - 2 ) = ( Y + -u 2 ) )
9 8 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y - 2 ) mod N ) = ( ( Y + -u 2 ) mod N ) )
10 eluz5nn 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. NN )
11 10 adantr 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> N e. NN )
12 simpr 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> Y e. I )
13 1zzd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 1 e. ZZ )
14 2z 
 |-  2 e. ZZ
15 14 a1i 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 2 e. ZZ )
16 15 znegcld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> -u 2 e. ZZ )
17 ax-1cn 
 |-  1 e. CC
18 2cn 
 |-  2 e. CC
19 17 18 subnegi 
 |-  ( 1 - -u 2 ) = ( 1 + 2 )
20 1p2e3 
 |-  ( 1 + 2 ) = 3
21 19 20 eqtri 
 |-  ( 1 - -u 2 ) = 3
22 21 fveq2i 
 |-  ( abs ` ( 1 - -u 2 ) ) = ( abs ` 3 )
23 3nn0 
 |-  3 e. NN0
24 23 nn0absidi 
 |-  ( abs ` 3 ) = 3
25 22 24 eqtri 
 |-  ( abs ` ( 1 - -u 2 ) ) = 3
26 3nn 
 |-  3 e. NN
27 26 a1i 
 |-  ( N e. ( ZZ>= ` 5 ) -> 3 e. NN )
28 eluz2 
 |-  ( N e. ( ZZ>= ` 5 ) <-> ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) )
29 3re 
 |-  3 e. RR
30 29 a1i 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 3 e. RR )
31 5re 
 |-  5 e. RR
32 31 a1i 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 5 e. RR )
33 zre 
 |-  ( N e. ZZ -> N e. RR )
34 33 adantr 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> N e. RR )
35 3lt5 
 |-  3 < 5
36 35 a1i 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 3 < 5 )
37 simpr 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 5 <_ N )
38 30 32 34 36 37 ltletrd 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 3 < N )
39 38 3adant1 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 3 < N )
40 28 39 sylbi 
 |-  ( N e. ( ZZ>= ` 5 ) -> 3 < N )
41 elfzo1 
 |-  ( 3 e. ( 1 ..^ N ) <-> ( 3 e. NN /\ N e. NN /\ 3 < N ) )
42 27 10 40 41 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 5 ) -> 3 e. ( 1 ..^ N ) )
43 42 adantr 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 3 e. ( 1 ..^ N ) )
44 25 43 eqeltrid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( abs ` ( 1 - -u 2 ) ) e. ( 1 ..^ N ) )
45 1 mod2addne 
 |-  ( ( N e. NN /\ ( Y e. I /\ 1 e. ZZ /\ -u 2 e. ZZ ) /\ ( abs ` ( 1 - -u 2 ) ) e. ( 1 ..^ N ) ) -> ( ( Y + 1 ) mod N ) =/= ( ( Y + -u 2 ) mod N ) )
46 11 12 13 16 44 45 syl131anc 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y + 1 ) mod N ) =/= ( ( Y + -u 2 ) mod N ) )
47 46 necomd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y + -u 2 ) mod N ) =/= ( ( Y + 1 ) mod N ) )
48 9 47 eqnetrd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y - 2 ) mod N ) =/= ( ( Y + 1 ) mod N ) )