Metamath Proof Explorer

Theorem modm1nem2

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

Ref Expression
Hypothesis modm1nep1.i 
|- I = ( 0 ..^ N )
Assertion modm1nem2 
|- ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y - 1 ) mod N ) =/= ( ( Y - 2 ) 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 1zzd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 1 e. ZZ )
6 5 znegcld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> -u 1 e. ZZ )
7 2z 
 |-  2 e. ZZ
8 7 a1i 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 2 e. ZZ )
9 8 znegcld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> -u 2 e. ZZ )
10 ax-1cn 
 |-  1 e. CC
11 2cn 
 |-  2 e. CC
12 neg2sub 
 |-  ( ( 1 e. CC /\ 2 e. CC ) -> ( -u 1 - -u 2 ) = ( 2 - 1 ) )
13 10 11 12 mp2an 
 |-  ( -u 1 - -u 2 ) = ( 2 - 1 )
14 2m1e1 
 |-  ( 2 - 1 ) = 1
15 13 14 eqtri 
 |-  ( -u 1 - -u 2 ) = 1
16 15 fveq2i 
 |-  ( abs ` ( -u 1 - -u 2 ) ) = ( abs ` 1 )
17 abs1 
 |-  ( abs ` 1 ) = 1
18 16 17 eqtri 
 |-  ( abs ` ( -u 1 - -u 2 ) ) = 1
19 eluz2 
 |-  ( N e. ( ZZ>= ` 5 ) <-> ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) )
20 1red 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 1 e. RR )
21 5re 
 |-  5 e. RR
22 21 a1i 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 5 e. RR )
23 zre 
 |-  ( N e. ZZ -> N e. RR )
24 23 adantr 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> N e. RR )
25 1lt5 
 |-  1 < 5
26 25 a1i 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 1 < 5 )
27 simpr 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 5 <_ N )
28 20 22 24 26 27 ltletrd 
 |-  ( ( N e. ZZ /\ 5 <_ N ) -> 1 < N )
29 28 3adant1 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 1 < N )
30 19 29 sylbi 
 |-  ( N e. ( ZZ>= ` 5 ) -> 1 < N )
31 1elfzo1 
 |-  ( 1 e. ( 1 ..^ N ) <-> ( N e. NN /\ 1 < N ) )
32 2 30 31 sylanbrc 
 |-  ( N e. ( ZZ>= ` 5 ) -> 1 e. ( 1 ..^ N ) )
33 32 adantr 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> 1 e. ( 1 ..^ N ) )
34 18 33 eqeltrid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( abs ` ( -u 1 - -u 2 ) ) e. ( 1 ..^ N ) )
35 1 mod2addne 
 |-  ( ( N e. NN /\ ( Y e. I /\ -u 1 e. ZZ /\ -u 2 e. ZZ ) /\ ( abs ` ( -u 1 - -u 2 ) ) e. ( 1 ..^ N ) ) -> ( ( Y + -u 1 ) mod N ) =/= ( ( Y + -u 2 ) mod N ) )
36 3 4 6 9 34 35 syl131anc 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y + -u 1 ) mod N ) =/= ( ( Y + -u 2 ) mod N ) )
37 elfzoelz 
 |-  ( Y e. ( 0 ..^ N ) -> Y e. ZZ )
38 37 1 eleq2s 
 |-  ( Y e. I -> Y e. ZZ )
39 38 zcnd 
 |-  ( Y e. I -> Y e. CC )
40 1cnd 
 |-  ( Y e. I -> 1 e. CC )
41 39 40 negsubd 
 |-  ( Y e. I -> ( Y + -u 1 ) = ( Y - 1 ) )
42 41 eqcomd 
 |-  ( Y e. I -> ( Y - 1 ) = ( Y + -u 1 ) )
43 42 oveq1d 
 |-  ( Y e. I -> ( ( Y - 1 ) mod N ) = ( ( Y + -u 1 ) mod N ) )
44 2cnd 
 |-  ( Y e. I -> 2 e. CC )
45 39 44 negsubd 
 |-  ( Y e. I -> ( Y + -u 2 ) = ( Y - 2 ) )
46 45 eqcomd 
 |-  ( Y e. I -> ( Y - 2 ) = ( Y + -u 2 ) )
47 46 oveq1d 
 |-  ( Y e. I -> ( ( Y - 2 ) mod N ) = ( ( Y + -u 2 ) mod N ) )
48 43 47 neeq12d 
 |-  ( Y e. I -> ( ( ( Y - 1 ) mod N ) =/= ( ( Y - 2 ) mod N ) <-> ( ( Y + -u 1 ) mod N ) =/= ( ( Y + -u 2 ) mod N ) ) )
49 48 adantl 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( ( Y - 1 ) mod N ) =/= ( ( Y - 2 ) mod N ) <-> ( ( Y + -u 1 ) mod N ) =/= ( ( Y + -u 2 ) mod N ) ) )
50 36 49 mpbird 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ Y e. I ) -> ( ( Y - 1 ) mod N ) =/= ( ( Y - 2 ) mod N ) )