Metamath Proof Explorer

Theorem gpgedgvtx1

Description: The edges starting at an inside vertex in a generalized Petersen graph G . (Contributed by AV, 2-Sep-2025)

Ref Expression
Hypotheses gpgedgvtx0.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgedgvtx0.g 
|- G = ( N gPetersenGr K )
gpgedgvtx0.v 
|- V = ( Vtx ` G )
gpgedgvtx0.e 
|- E = ( Edg ` G )
Assertion gpgedgvtx1 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) )

Proof

Step Hyp Ref Expression
1 gpgedgvtx0.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgedgvtx0.g 
 |-  G = ( N gPetersenGr K )
3 gpgedgvtx0.v 
 |-  V = ( Vtx ` G )
4 gpgedgvtx0.e 
 |-  E = ( Edg ` G )
5 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
6 5 1 2 3 gpgvtxel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V <-> E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. ) )
7 fveq2 
 |-  ( X = <. x , y >. -> ( 1st ` X ) = ( 1st ` <. x , y >. ) )
8 7 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ X = <. x , y >. ) -> ( 1st ` X ) = ( 1st ` <. x , y >. ) )
9 vex 
 |-  x e. _V
10 vex 
 |-  y e. _V
11 9 10 op1st 
 |-  ( 1st ` <. x , y >. ) = x
12 8 11 eqtrdi 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ X = <. x , y >. ) -> ( 1st ` X ) = x )
13 12 eqeq1d 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ X = <. x , y >. ) -> ( ( 1st ` X ) = 1 <-> x = 1 ) )
14 opeq1 
 |-  ( x = 1 -> <. x , y >. = <. 1 , y >. )
15 14 eqeq2d 
 |-  ( x = 1 -> ( X = <. x , y >. <-> X = <. 1 , y >. ) )
16 15 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ x = 1 ) -> ( X = <. x , y >. <-> X = <. 1 , y >. ) )
17 opeq2 
 |-  ( z = y -> <. 0 , z >. = <. 0 , y >. )
18 oveq1 
 |-  ( z = y -> ( z + 1 ) = ( y + 1 ) )
19 18 oveq1d 
 |-  ( z = y -> ( ( z + 1 ) mod N ) = ( ( y + 1 ) mod N ) )
20 19 opeq2d 
 |-  ( z = y -> <. 0 , ( ( z + 1 ) mod N ) >. = <. 0 , ( ( y + 1 ) mod N ) >. )
21 17 20 preq12d 
 |-  ( z = y -> { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } )
22 21 eqeq2d 
 |-  ( z = y -> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } ) )
23 opeq2 
 |-  ( z = y -> <. 1 , z >. = <. 1 , y >. )
24 17 23 preq12d 
 |-  ( z = y -> { <. 0 , z >. , <. 1 , z >. } = { <. 0 , y >. , <. 1 , y >. } )
25 24 eqeq2d 
 |-  ( z = y -> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } ) )
26 oveq1 
 |-  ( z = y -> ( z + K ) = ( y + K ) )
27 26 oveq1d 
 |-  ( z = y -> ( ( z + K ) mod N ) = ( ( y + K ) mod N ) )
28 27 opeq2d 
 |-  ( z = y -> <. 1 , ( ( z + K ) mod N ) >. = <. 1 , ( ( y + K ) mod N ) >. )
29 23 28 preq12d 
 |-  ( z = y -> { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } )
30 29 eqeq2d 
 |-  ( z = y -> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
31 22 25 30 3orbi123d 
 |-  ( z = y -> ( ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
32 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> y e. ( 0 ..^ N ) )
33 eqid 
 |-  { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. }
34 33 3mix3i 
 |-  ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } )
35 34 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
36 31 32 35 rspcedvdw 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
37 21 eqeq2d 
 |-  ( z = y -> ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } ) )
38 24 eqeq2d 
 |-  ( z = y -> ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 1 , y >. } ) )
39 29 eqeq2d 
 |-  ( z = y -> ( { <. 1 , y >. , <. 0 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 1 , y >. , <. 0 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
40 37 38 39 3orbi123d 
 |-  ( z = y -> ( ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
41 prcom 
 |-  { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 1 , y >. }
42 41 3mix2i 
 |-  ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } )
43 42 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
44 40 32 43 rspcedvdw 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
45 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
46 45 1 eleq2s 
 |-  ( K e. J -> K e. ZZ )
47 46 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K e. ZZ )
48 47 anim1ci 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( y e. ( 0 ..^ N ) /\ K e. ZZ ) )
49 fzospliti 
 |-  ( ( y e. ( 0 ..^ N ) /\ K e. ZZ ) -> ( y e. ( 0 ..^ K ) \/ y e. ( K ..^ N ) ) )
50 48 49 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( y e. ( 0 ..^ K ) \/ y e. ( K ..^ N ) ) )
51 50 ex 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( y e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ K ) \/ y e. ( K ..^ N ) ) ) )
52 opeq2 
 |-  ( z = ( ( N + y ) - K ) -> <. 0 , z >. = <. 0 , ( ( N + y ) - K ) >. )
53 oveq1 
 |-  ( z = ( ( N + y ) - K ) -> ( z + 1 ) = ( ( ( N + y ) - K ) + 1 ) )
54 53 oveq1d 
 |-  ( z = ( ( N + y ) - K ) -> ( ( z + 1 ) mod N ) = ( ( ( ( N + y ) - K ) + 1 ) mod N ) )
55 54 opeq2d 
 |-  ( z = ( ( N + y ) - K ) -> <. 0 , ( ( z + 1 ) mod N ) >. = <. 0 , ( ( ( ( N + y ) - K ) + 1 ) mod N ) >. )
56 52 55 preq12d 
 |-  ( z = ( ( N + y ) - K ) -> { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 0 , ( ( ( ( N + y ) - K ) + 1 ) mod N ) >. } )
57 56 eqeq2d 
 |-  ( z = ( ( N + y ) - K ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 0 , ( ( ( ( N + y ) - K ) + 1 ) mod N ) >. } ) )
58 opeq2 
 |-  ( z = ( ( N + y ) - K ) -> <. 1 , z >. = <. 1 , ( ( N + y ) - K ) >. )
59 52 58 preq12d 
 |-  ( z = ( ( N + y ) - K ) -> { <. 0 , z >. , <. 1 , z >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 1 , ( ( N + y ) - K ) >. } )
60 59 eqeq2d 
 |-  ( z = ( ( N + y ) - K ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 1 , ( ( N + y ) - K ) >. } ) )
61 oveq1 
 |-  ( z = ( ( N + y ) - K ) -> ( z + K ) = ( ( ( N + y ) - K ) + K ) )
62 61 oveq1d 
 |-  ( z = ( ( N + y ) - K ) -> ( ( z + K ) mod N ) = ( ( ( ( N + y ) - K ) + K ) mod N ) )
63 62 opeq2d 
 |-  ( z = ( ( N + y ) - K ) -> <. 1 , ( ( z + K ) mod N ) >. = <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. )
64 58 63 preq12d 
 |-  ( z = ( ( N + y ) - K ) -> { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } = { <. 1 , ( ( N + y ) - K ) >. , <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. } )
65 64 eqeq2d 
 |-  ( z = ( ( N + y ) - K ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( ( N + y ) - K ) >. , <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. } ) )
66 57 60 65 3orbi123d 
 |-  ( z = ( ( N + y ) - K ) -> ( ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 0 , ( ( ( ( N + y ) - K ) + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 1 , ( ( N + y ) - K ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( ( N + y ) - K ) >. , <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. } ) ) )
67 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
68 67 nnzd 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
69 68 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. ZZ )
70 69 zcnd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. CC )
71 70 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> N e. CC )
72 elfzoel2 
 |-  ( y e. ( 0 ..^ K ) -> K e. ZZ )
73 72 zcnd 
 |-  ( y e. ( 0 ..^ K ) -> K e. CC )
74 73 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> K e. CC )
75 elfzoelz 
 |-  ( y e. ( 0 ..^ K ) -> y e. ZZ )
76 75 zcnd 
 |-  ( y e. ( 0 ..^ K ) -> y e. CC )
77 76 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> y e. CC )
78 71 74 77 subsub3d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( N - ( K - y ) ) = ( ( N + y ) - K ) )
79 1zzd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> 1 e. ZZ )
80 69 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> N e. ZZ )
81 72 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> K e. ZZ )
82 75 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> y e. ZZ )
83 81 82 zsubcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( K - y ) e. ZZ )
84 elfzo0subge1 
 |-  ( y e. ( 0 ..^ K ) -> 1 <_ ( K - y ) )
85 84 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> 1 <_ ( K - y ) )
86 83 zred 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( K - y ) e. RR )
87 81 zred 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> K e. RR )
88 80 zred 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> N e. RR )
89 elfzo0suble 
 |-  ( y e. ( 0 ..^ K ) -> ( K - y ) <_ K )
90 89 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( K - y ) <_ K )
91 1 5 gpgedgvtx1lem 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K e. ( 0 ..^ N ) )
92 elfzo0le 
 |-  ( K e. ( 0 ..^ N ) -> K <_ N )
93 91 92 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K <_ N )
94 93 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> K <_ N )
95 86 87 88 90 94 letrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( K - y ) <_ N )
96 79 80 83 85 95 elfzd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( K - y ) e. ( 1 ... N ) )
97 ubmelfzo 
 |-  ( ( K - y ) e. ( 1 ... N ) -> ( N - ( K - y ) ) e. ( 0 ..^ N ) )
98 96 97 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( N - ( K - y ) ) e. ( 0 ..^ N ) )
99 78 98 eqeltrrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( ( N + y ) - K ) e. ( 0 ..^ N ) )
100 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
101 100 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. CC )
102 101 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> N e. CC )
103 102 77 addcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( N + y ) e. CC )
104 103 74 npcand 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( ( ( N + y ) - K ) + K ) = ( N + y ) )
105 104 oveq1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( ( ( ( N + y ) - K ) + K ) mod N ) = ( ( N + y ) mod N ) )
106 elfzonn0 
 |-  ( y e. ( 0 ..^ K ) -> y e. NN0 )
107 106 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> y e. NN0 )
108 67 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. NN )
109 108 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> N e. NN )
110 elfzouz2 
 |-  ( K e. ( 0 ..^ N ) -> N e. ( ZZ>= ` K ) )
111 fzoss2 
 |-  ( N e. ( ZZ>= ` K ) -> ( 0 ..^ K ) C_ ( 0 ..^ N ) )
112 110 111 syl 
 |-  ( K e. ( 0 ..^ N ) -> ( 0 ..^ K ) C_ ( 0 ..^ N ) )
113 112 sseld 
 |-  ( K e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ K ) -> y e. ( 0 ..^ N ) ) )
114 elfzolt2 
 |-  ( y e. ( 0 ..^ N ) -> y < N )
115 113 114 syl6 
 |-  ( K e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ K ) -> y < N ) )
116 91 115 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( y e. ( 0 ..^ K ) -> y < N ) )
117 116 imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> y < N )
118 addmodid 
 |-  ( ( y e. NN0 /\ N e. NN /\ y < N ) -> ( ( N + y ) mod N ) = y )
119 107 109 117 118 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( ( N + y ) mod N ) = y )
120 105 119 eqtr2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> y = ( ( ( ( N + y ) - K ) + K ) mod N ) )
121 120 opeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> <. 1 , y >. = <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. )
122 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> y e. ( 0 ..^ K ) )
123 elfzolt2 
 |-  ( K e. ( 0 ..^ N ) -> K < N )
124 91 123 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K < N )
125 124 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> K < N )
126 submodlt 
 |-  ( ( N e. NN /\ y e. ( 0 ..^ K ) /\ K < N ) -> ( ( y - K ) mod N ) = ( ( N + y ) - K ) )
127 109 122 125 126 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( ( y - K ) mod N ) = ( ( N + y ) - K ) )
128 127 opeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> <. 1 , ( ( y - K ) mod N ) >. = <. 1 , ( ( N + y ) - K ) >. )
129 121 128 preq12d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. , <. 1 , ( ( N + y ) - K ) >. } )
130 prcom 
 |-  { <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. , <. 1 , ( ( N + y ) - K ) >. } = { <. 1 , ( ( N + y ) - K ) >. , <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. }
131 129 130 eqtrdi 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( ( N + y ) - K ) >. , <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. } )
132 131 3mix3d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 0 , ( ( ( ( N + y ) - K ) + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( ( N + y ) - K ) >. , <. 1 , ( ( N + y ) - K ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( ( N + y ) - K ) >. , <. 1 , ( ( ( ( N + y ) - K ) + K ) mod N ) >. } ) )
133 66 99 132 rspcedvdw 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ K ) ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
134 133 ex 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( y e. ( 0 ..^ K ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
135 opeq2 
 |-  ( z = ( y - K ) -> <. 0 , z >. = <. 0 , ( y - K ) >. )
136 oveq1 
 |-  ( z = ( y - K ) -> ( z + 1 ) = ( ( y - K ) + 1 ) )
137 136 oveq1d 
 |-  ( z = ( y - K ) -> ( ( z + 1 ) mod N ) = ( ( ( y - K ) + 1 ) mod N ) )
138 137 opeq2d 
 |-  ( z = ( y - K ) -> <. 0 , ( ( z + 1 ) mod N ) >. = <. 0 , ( ( ( y - K ) + 1 ) mod N ) >. )
139 135 138 preq12d 
 |-  ( z = ( y - K ) -> { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } = { <. 0 , ( y - K ) >. , <. 0 , ( ( ( y - K ) + 1 ) mod N ) >. } )
140 139 eqeq2d 
 |-  ( z = ( y - K ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( y - K ) >. , <. 0 , ( ( ( y - K ) + 1 ) mod N ) >. } ) )
141 opeq2 
 |-  ( z = ( y - K ) -> <. 1 , z >. = <. 1 , ( y - K ) >. )
142 135 141 preq12d 
 |-  ( z = ( y - K ) -> { <. 0 , z >. , <. 1 , z >. } = { <. 0 , ( y - K ) >. , <. 1 , ( y - K ) >. } )
143 142 eqeq2d 
 |-  ( z = ( y - K ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( y - K ) >. , <. 1 , ( y - K ) >. } ) )
144 oveq1 
 |-  ( z = ( y - K ) -> ( z + K ) = ( ( y - K ) + K ) )
145 144 oveq1d 
 |-  ( z = ( y - K ) -> ( ( z + K ) mod N ) = ( ( ( y - K ) + K ) mod N ) )
146 145 opeq2d 
 |-  ( z = ( y - K ) -> <. 1 , ( ( z + K ) mod N ) >. = <. 1 , ( ( ( y - K ) + K ) mod N ) >. )
147 141 146 preq12d 
 |-  ( z = ( y - K ) -> { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } = { <. 1 , ( y - K ) >. , <. 1 , ( ( ( y - K ) + K ) mod N ) >. } )
148 147 eqeq2d 
 |-  ( z = ( y - K ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( y - K ) >. , <. 1 , ( ( ( y - K ) + K ) mod N ) >. } ) )
149 140 143 148 3orbi123d 
 |-  ( z = ( y - K ) -> ( ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( y - K ) >. , <. 0 , ( ( ( y - K ) + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( y - K ) >. , <. 1 , ( y - K ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( y - K ) >. , <. 1 , ( ( ( y - K ) + K ) mod N ) >. } ) ) )
150 elfzo1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
151 150 simp1bi 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. NN )
152 151 nnnn0d 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. NN0 )
153 152 1 eleq2s 
 |-  ( K e. J -> K e. NN0 )
154 153 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K e. NN0 )
155 elfzoextl 
 |-  ( ( y e. ( K ..^ N ) /\ K e. NN0 ) -> y e. ( K ..^ ( K + N ) ) )
156 154 155 sylan2 
 |-  ( ( y e. ( K ..^ N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> y e. ( K ..^ ( K + N ) ) )
157 156 ancoms 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> y e. ( K ..^ ( K + N ) ) )
158 108 nnzd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. ZZ )
159 158 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> N e. ZZ )
160 fzosubel3 
 |-  ( ( y e. ( K ..^ ( K + N ) ) /\ N e. ZZ ) -> ( y - K ) e. ( 0 ..^ N ) )
161 157 159 160 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( y - K ) e. ( 0 ..^ N ) )
162 elfzoelz 
 |-  ( y e. ( K ..^ N ) -> y e. ZZ )
163 162 zcnd 
 |-  ( y e. ( K ..^ N ) -> y e. CC )
164 elfzoel1 
 |-  ( y e. ( K ..^ N ) -> K e. ZZ )
165 164 zcnd 
 |-  ( y e. ( K ..^ N ) -> K e. CC )
166 163 165 npcand 
 |-  ( y e. ( K ..^ N ) -> ( ( y - K ) + K ) = y )
167 166 oveq1d 
 |-  ( y e. ( K ..^ N ) -> ( ( ( y - K ) + K ) mod N ) = ( y mod N ) )
168 167 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( ( ( y - K ) + K ) mod N ) = ( y mod N ) )
169 67 nnrpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR+ )
170 169 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. RR+ )
171 162 zred 
 |-  ( y e. ( K ..^ N ) -> y e. RR )
172 170 171 anim12ci 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( y e. RR /\ N e. RR+ ) )
173 elfzole1 
 |-  ( y e. ( K ..^ N ) -> K <_ y )
174 173 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> K <_ y )
175 0red 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) /\ K <_ y ) -> 0 e. RR )
176 164 zred 
 |-  ( y e. ( K ..^ N ) -> K e. RR )
177 176 ad2antlr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) /\ K <_ y ) -> K e. RR )
178 171 ad2antlr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) /\ K <_ y ) -> y e. RR )
179 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
180 179 nn0ge0d 
 |-  ( K e. NN -> 0 <_ K )
181 151 180 syl 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> 0 <_ K )
182 181 1 eleq2s 
 |-  ( K e. J -> 0 <_ K )
183 182 ad3antlr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) /\ K <_ y ) -> 0 <_ K )
184 simpr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) /\ K <_ y ) -> K <_ y )
185 175 177 178 183 184 letrd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) /\ K <_ y ) -> 0 <_ y )
186 174 185 mpdan 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> 0 <_ y )
187 elfzolt2 
 |-  ( y e. ( K ..^ N ) -> y < N )
188 187 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> y < N )
189 modid 
 |-  ( ( ( y e. RR /\ N e. RR+ ) /\ ( 0 <_ y /\ y < N ) ) -> ( y mod N ) = y )
190 172 186 188 189 syl12anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( y mod N ) = y )
191 168 190 eqtr2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> y = ( ( ( y - K ) + K ) mod N ) )
192 191 opeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> <. 1 , y >. = <. 1 , ( ( ( y - K ) + K ) mod N ) >. )
193 171 176 resubcld 
 |-  ( y e. ( K ..^ N ) -> ( y - K ) e. RR )
194 170 193 anim12ci 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( ( y - K ) e. RR /\ N e. RR+ ) )
195 elfzo2 
 |-  ( y e. ( K ..^ N ) <-> ( y e. ( ZZ>= ` K ) /\ N e. ZZ /\ y < N ) )
196 eluz2 
 |-  ( y e. ( ZZ>= ` K ) <-> ( K e. ZZ /\ y e. ZZ /\ K <_ y ) )
197 simp13 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> K <_ y )
198 zre 
 |-  ( K e. ZZ -> K e. RR )
199 zre 
 |-  ( y e. ZZ -> y e. RR )
200 198 199 anim12ci 
 |-  ( ( K e. ZZ /\ y e. ZZ ) -> ( y e. RR /\ K e. RR ) )
201 200 3adant3 
 |-  ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) -> ( y e. RR /\ K e. RR ) )
202 201 3ad2ant1 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> ( y e. RR /\ K e. RR ) )
203 subge0 
 |-  ( ( y e. RR /\ K e. RR ) -> ( 0 <_ ( y - K ) <-> K <_ y ) )
204 202 203 syl 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> ( 0 <_ ( y - K ) <-> K <_ y ) )
205 197 204 mpbird 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> 0 <_ ( y - K ) )
206 199 3ad2ant2 
 |-  ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) -> y e. RR )
207 206 3ad2ant1 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> y e. RR )
208 198 3ad2ant1 
 |-  ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) -> K e. RR )
209 208 3ad2ant1 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> K e. RR )
210 207 209 resubcld 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> ( y - K ) e. RR )
211 zre 
 |-  ( N e. ZZ -> N e. RR )
212 211 adantr 
 |-  ( ( N e. ZZ /\ y < N ) -> N e. RR )
213 212 3ad2ant2 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> N e. RR )
214 nnrp 
 |-  ( K e. NN -> K e. RR+ )
215 214 3ad2ant1 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) -> K e. RR+ )
216 150 215 sylbi 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. RR+ )
217 216 1 eleq2s 
 |-  ( K e. J -> K e. RR+ )
218 217 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> K e. RR+ )
219 218 3ad2ant3 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> K e. RR+ )
220 207 219 ltsubrpd 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> ( y - K ) < y )
221 simp2r 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> y < N )
222 210 207 213 220 221 lttrd 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> ( y - K ) < N )
223 205 222 jca 
 |-  ( ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) /\ ( N e. ZZ /\ y < N ) /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J ) ) -> ( 0 <_ ( y - K ) /\ ( y - K ) < N ) )
224 223 3exp 
 |-  ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) -> ( ( N e. ZZ /\ y < N ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 0 <_ ( y - K ) /\ ( y - K ) < N ) ) ) )
225 224 expd 
 |-  ( ( K e. ZZ /\ y e. ZZ /\ K <_ y ) -> ( N e. ZZ -> ( y < N -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 0 <_ ( y - K ) /\ ( y - K ) < N ) ) ) ) )
226 196 225 sylbi 
 |-  ( y e. ( ZZ>= ` K ) -> ( N e. ZZ -> ( y < N -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 0 <_ ( y - K ) /\ ( y - K ) < N ) ) ) ) )
227 226 3imp 
 |-  ( ( y e. ( ZZ>= ` K ) /\ N e. ZZ /\ y < N ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 0 <_ ( y - K ) /\ ( y - K ) < N ) ) )
228 195 227 sylbi 
 |-  ( y e. ( K ..^ N ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( 0 <_ ( y - K ) /\ ( y - K ) < N ) ) )
229 228 impcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( 0 <_ ( y - K ) /\ ( y - K ) < N ) )
230 modid 
 |-  ( ( ( ( y - K ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( y - K ) /\ ( y - K ) < N ) ) -> ( ( y - K ) mod N ) = ( y - K ) )
231 194 229 230 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( ( y - K ) mod N ) = ( y - K ) )
232 231 opeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> <. 1 , ( ( y - K ) mod N ) >. = <. 1 , ( y - K ) >. )
233 192 232 preq12d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( ( ( y - K ) + K ) mod N ) >. , <. 1 , ( y - K ) >. } )
234 prcom 
 |-  { <. 1 , ( ( ( y - K ) + K ) mod N ) >. , <. 1 , ( y - K ) >. } = { <. 1 , ( y - K ) >. , <. 1 , ( ( ( y - K ) + K ) mod N ) >. }
235 233 234 eqtrdi 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( y - K ) >. , <. 1 , ( ( ( y - K ) + K ) mod N ) >. } )
236 235 3mix3d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( y - K ) >. , <. 0 , ( ( ( y - K ) + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , ( y - K ) >. , <. 1 , ( y - K ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , ( y - K ) >. , <. 1 , ( ( ( y - K ) + K ) mod N ) >. } ) )
237 149 161 236 rspcedvdw 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( K ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
238 237 ex 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( y e. ( K ..^ N ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
239 134 238 jaod 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( y e. ( 0 ..^ K ) \/ y e. ( K ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
240 51 239 syld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( y e. ( 0 ..^ N ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
241 240 imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
242 5 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } e. E <-> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
243 5 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 1 , y >. , <. 0 , y >. } e. E <-> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
244 5 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } e. E <-> E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
245 242 243 244 3anbi123d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } e. E /\ { <. 1 , y >. , <. 0 , y >. } e. E /\ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } e. E ) <-> ( E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) ) )
246 245 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } e. E /\ { <. 1 , y >. , <. 0 , y >. } e. E /\ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } e. E ) <-> ( E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 0 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) ) )
247 36 44 241 246 mpbir3and 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } e. E /\ { <. 1 , y >. , <. 0 , y >. } e. E /\ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } e. E ) )
248 247 adantrl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } e. E /\ { <. 1 , y >. , <. 0 , y >. } e. E /\ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } e. E ) )
249 id 
 |-  ( X = <. 1 , y >. -> X = <. 1 , y >. )
250 1ex 
 |-  1 e. _V
251 250 10 op2ndd 
 |-  ( X = <. 1 , y >. -> ( 2nd ` X ) = y )
252 251 oveq1d 
 |-  ( X = <. 1 , y >. -> ( ( 2nd ` X ) + K ) = ( y + K ) )
253 252 oveq1d 
 |-  ( X = <. 1 , y >. -> ( ( ( 2nd ` X ) + K ) mod N ) = ( ( y + K ) mod N ) )
254 253 opeq2d 
 |-  ( X = <. 1 , y >. -> <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. = <. 1 , ( ( y + K ) mod N ) >. )
255 249 254 preq12d 
 |-  ( X = <. 1 , y >. -> { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } )
256 255 eleq1d 
 |-  ( X = <. 1 , y >. -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E <-> { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } e. E ) )
257 251 opeq2d 
 |-  ( X = <. 1 , y >. -> <. 0 , ( 2nd ` X ) >. = <. 0 , y >. )
258 249 257 preq12d 
 |-  ( X = <. 1 , y >. -> { X , <. 0 , ( 2nd ` X ) >. } = { <. 1 , y >. , <. 0 , y >. } )
259 258 eleq1d 
 |-  ( X = <. 1 , y >. -> ( { X , <. 0 , ( 2nd ` X ) >. } e. E <-> { <. 1 , y >. , <. 0 , y >. } e. E ) )
260 251 oveq1d 
 |-  ( X = <. 1 , y >. -> ( ( 2nd ` X ) - K ) = ( y - K ) )
261 260 oveq1d 
 |-  ( X = <. 1 , y >. -> ( ( ( 2nd ` X ) - K ) mod N ) = ( ( y - K ) mod N ) )
262 261 opeq2d 
 |-  ( X = <. 1 , y >. -> <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. = <. 1 , ( ( y - K ) mod N ) >. )
263 249 262 preq12d 
 |-  ( X = <. 1 , y >. -> { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } )
264 263 eleq1d 
 |-  ( X = <. 1 , y >. -> ( { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E <-> { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } e. E ) )
265 256 259 264 3anbi123d 
 |-  ( X = <. 1 , y >. -> ( ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) <-> ( { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } e. E /\ { <. 1 , y >. , <. 0 , y >. } e. E /\ { <. 1 , y >. , <. 1 , ( ( y - K ) mod N ) >. } e. E ) ) )
266 248 265 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( X = <. 1 , y >. -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) )
267 266 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ x = 1 ) -> ( X = <. 1 , y >. -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) )
268 16 267 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ x = 1 ) -> ( X = <. x , y >. -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) )
269 268 impancom 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ X = <. x , y >. ) -> ( x = 1 -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) )
270 13 269 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ X = <. x , y >. ) -> ( ( 1st ` X ) = 1 -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) )
271 270 ex 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( X = <. x , y >. -> ( ( 1st ` X ) = 1 -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) ) )
272 271 rexlimdvva 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. -> ( ( 1st ` X ) = 1 -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) ) )
273 6 272 sylbid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V -> ( ( 1st ` X ) = 1 -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) ) ) )
274 273 imp32 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 1 ) ) -> ( { X , <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. } e. E /\ { X , <. 0 , ( 2nd ` X ) >. } e. E /\ { X , <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. } e. E ) )