Metamath Proof Explorer

Theorem modm1p1ne

Description: If an integer minus one equals another integer plus one modulo an integer greater than 4, then the first integer plus one is not equal to the second integer minus one modulo the same modulus. (Contributed by AV, 15-Nov-2025)

Ref Expression
Hypothesis modm1nep1.i 
|- I = ( 0 ..^ N )
Assertion modm1p1ne 
|- ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> ( ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) -> ( ( Y + 1 ) mod N ) =/= ( ( X - 1 ) mod N ) ) )

Proof

Step Hyp Ref Expression
1 modm1nep1.i 
 |-  I = ( 0 ..^ N )
2 eluz2 
 |-  ( N e. ( ZZ>= ` 5 ) <-> ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) )
3 4nn0 
 |-  4 e. NN0
4 3 a1i 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 4 e. NN0 )
5 simp2 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> N e. ZZ )
6 0red 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 0 e. RR )
7 5re 
 |-  5 e. RR
8 7 a1i 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 5 e. RR )
9 zre 
 |-  ( N e. ZZ -> N e. RR )
10 9 3ad2ant2 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> N e. RR )
11 5pos 
 |-  0 < 5
12 11 a1i 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 0 < 5 )
13 simp3 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 5 <_ N )
14 6 8 10 12 13 ltletrd 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 0 < N )
15 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
16 5 14 15 sylanbrc 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> N e. NN )
17 4re 
 |-  4 e. RR
18 17 a1i 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 4 e. RR )
19 4lt5 
 |-  4 < 5
20 19 a1i 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 4 < 5 )
21 18 8 10 20 13 ltletrd 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 4 < N )
22 elfzo0 
 |-  ( 4 e. ( 0 ..^ N ) <-> ( 4 e. NN0 /\ N e. NN /\ 4 < N ) )
23 4 16 21 22 syl3anbrc 
 |-  ( ( 5 e. ZZ /\ N e. ZZ /\ 5 <_ N ) -> 4 e. ( 0 ..^ N ) )
24 2 23 sylbi 
 |-  ( N e. ( ZZ>= ` 5 ) -> 4 e. ( 0 ..^ N ) )
25 zmodidfzoimp 
 |-  ( 4 e. ( 0 ..^ N ) -> ( 4 mod N ) = 4 )
26 24 25 syl 
 |-  ( N e. ( ZZ>= ` 5 ) -> ( 4 mod N ) = 4 )
27 4ne0 
 |-  4 =/= 0
28 27 a1i 
 |-  ( N e. ( ZZ>= ` 5 ) -> 4 =/= 0 )
29 26 28 eqnetrd 
 |-  ( N e. ( ZZ>= ` 5 ) -> ( 4 mod N ) =/= 0 )
30 df-ne 
 |-  ( ( ( 4 x. 1 ) mod N ) =/= 0 <-> -. ( ( 4 x. 1 ) mod N ) = 0 )
31 4cn 
 |-  4 e. CC
32 31 mulridi 
 |-  ( 4 x. 1 ) = 4
33 32 oveq1i 
 |-  ( ( 4 x. 1 ) mod N ) = ( 4 mod N )
34 33 neeq1i 
 |-  ( ( ( 4 x. 1 ) mod N ) =/= 0 <-> ( 4 mod N ) =/= 0 )
35 30 34 bitr3i 
 |-  ( -. ( ( 4 x. 1 ) mod N ) = 0 <-> ( 4 mod N ) =/= 0 )
36 29 35 sylibr 
 |-  ( N e. ( ZZ>= ` 5 ) -> -. ( ( 4 x. 1 ) mod N ) = 0 )
37 36 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> -. ( ( 4 x. 1 ) mod N ) = 0 )
38 37 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) /\ ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> -. ( ( 4 x. 1 ) mod N ) = 0 )
39 uzuzle35 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. ( ZZ>= ` 3 ) )
40 eluz3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
41 39 40 syl 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. NN )
42 41 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> N e. NN )
43 elfzoelz 
 |-  ( X e. ( 0 ..^ N ) -> X e. ZZ )
44 43 1 eleq2s 
 |-  ( X e. I -> X e. ZZ )
45 44 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> X e. ZZ )
46 elfzoelz 
 |-  ( Y e. ( 0 ..^ N ) -> Y e. ZZ )
47 46 1 eleq2s 
 |-  ( Y e. I -> Y e. ZZ )
48 47 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> Y e. ZZ )
49 1zzd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> 1 e. ZZ )
50 modmkpkne 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ 1 e. ZZ ) ) -> ( ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) <-> ( ( 4 x. 1 ) mod N ) = 0 ) ) )
51 42 45 48 49 50 syl13anc 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> ( ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) <-> ( ( 4 x. 1 ) mod N ) = 0 ) ) )
52 51 imp 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) /\ ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) <-> ( ( 4 x. 1 ) mod N ) = 0 ) )
53 38 52 mtbird 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) /\ ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> -. ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) )
54 53 neqned 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) /\ ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> ( ( Y + 1 ) mod N ) =/= ( ( X - 1 ) mod N ) )
55 54 ex 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ X e. I /\ Y e. I ) -> ( ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) -> ( ( Y + 1 ) mod N ) =/= ( ( X - 1 ) mod N ) ) )