Metamath Proof Explorer

Theorem modmknepk

Description: A nonnegative integer less than the modulus plus/minus a positive integer less than (the ceiling of) half of the modulus are not equal modulo the modulus. For this theorem, it is essential that K < ( N / 2 ) ! (Contributed by AV, 3-Sep-2025) (Revised by AV, 15-Nov-2025)

Ref Expression
Hypotheses modmknepk.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
modmknepk.i 
|- I = ( 0 ..^ N )
Assertion modmknepk 
|- ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ K e. J ) -> ( ( Y - K ) mod N ) =/= ( ( Y + K ) mod N ) )

Proof

Step Hyp Ref Expression
1 modmknepk.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 modmknepk.i 
 |-  I = ( 0 ..^ N )
3 eluz3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
4 3 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ K e. J ) -> N e. NN )
5 elfzoelz 
 |-  ( Y e. ( 0 ..^ N ) -> Y e. ZZ )
6 5 2 eleq2s 
 |-  ( Y e. I -> Y e. ZZ )
7 6 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ K e. J ) -> Y e. ZZ )
8 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
9 8 1 eleq2s 
 |-  ( K e. J -> K e. ZZ )
10 9 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ K e. J ) -> K e. ZZ )
11 9 zcnd 
 |-  ( K e. J -> K e. CC )
12 11 2timesd 
 |-  ( K e. J -> ( 2 x. K ) = ( K + K ) )
13 12 eqcomd 
 |-  ( K e. J -> ( K + K ) = ( 2 x. K ) )
14 13 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( K + K ) = ( 2 x. K ) )
15 1red 
 |-  ( K e. J -> 1 e. RR )
16 9 zred 
 |-  ( K e. J -> K e. RR )
17 2z 
 |-  2 e. ZZ
18 17 a1i 
 |-  ( K e. J -> 2 e. ZZ )
19 18 9 zmulcld 
 |-  ( K e. J -> ( 2 x. K ) e. ZZ )
20 19 zred 
 |-  ( K e. J -> ( 2 x. K ) e. RR )
21 elfzole1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> 1 <_ K )
22 21 1 eleq2s 
 |-  ( K e. J -> 1 <_ K )
23 elfzo1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
24 23 simp1bi 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. NN )
25 24 1 eleq2s 
 |-  ( K e. J -> K e. NN )
26 25 nnnn0d 
 |-  ( K e. J -> K e. NN0 )
27 nn0le2x 
 |-  ( K e. NN0 -> K <_ ( 2 x. K ) )
28 26 27 syl 
 |-  ( K e. J -> K <_ ( 2 x. K ) )
29 15 16 20 22 28 letrd 
 |-  ( K e. J -> 1 <_ ( 2 x. K ) )
30 29 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> 1 <_ ( 2 x. K ) )
31 1 eleq2i 
 |-  ( K e. J <-> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
32 2tceilhalfelfzo1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( 2 x. K ) < N )
33 31 32 sylan2b 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 2 x. K ) < N )
34 30 33 jca 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 1 <_ ( 2 x. K ) /\ ( 2 x. K ) < N ) )
35 breq2 
 |-  ( ( K + K ) = ( 2 x. K ) -> ( 1 <_ ( K + K ) <-> 1 <_ ( 2 x. K ) ) )
36 breq1 
 |-  ( ( K + K ) = ( 2 x. K ) -> ( ( K + K ) < N <-> ( 2 x. K ) < N ) )
37 35 36 anbi12d 
 |-  ( ( K + K ) = ( 2 x. K ) -> ( ( 1 <_ ( K + K ) /\ ( K + K ) < N ) <-> ( 1 <_ ( 2 x. K ) /\ ( 2 x. K ) < N ) ) )
38 34 37 syl5ibrcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( K + K ) = ( 2 x. K ) -> ( 1 <_ ( K + K ) /\ ( K + K ) < N ) ) )
39 14 38 mpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 1 <_ ( K + K ) /\ ( K + K ) < N ) )
40 39 3adant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ K e. J ) -> ( 1 <_ ( K + K ) /\ ( K + K ) < N ) )
41 submodneaddmod 
 |-  ( ( N e. NN /\ ( Y e. ZZ /\ K e. ZZ /\ K e. ZZ ) /\ ( 1 <_ ( K + K ) /\ ( K + K ) < N ) ) -> ( ( Y + K ) mod N ) =/= ( ( Y - K ) mod N ) )
42 41 necomd 
 |-  ( ( N e. NN /\ ( Y e. ZZ /\ K e. ZZ /\ K e. ZZ ) /\ ( 1 <_ ( K + K ) /\ ( K + K ) < N ) ) -> ( ( Y - K ) mod N ) =/= ( ( Y + K ) mod N ) )
43 4 7 10 10 40 42 syl131anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ K e. J ) -> ( ( Y - K ) mod N ) =/= ( ( Y + K ) mod N ) )