Metamath Proof Explorer

Theorem gpgedgvtx0

Description: The edges starting at an outside vertex in a generalized Petersen graph G . (Contributed by AV, 29-Aug-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 gpgedgvtx0 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) 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 ) = 0 <-> x = 0 ) )
14 opeq1 
 |-  ( x = 0 -> <. x , y >. = <. 0 , y >. )
15 14 eqeq2d 
 |-  ( x = 0 -> ( X = <. x , y >. <-> X = <. 0 , y >. ) )
16 15 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ x = 0 ) -> ( X = <. x , y >. <-> X = <. 0 , y >. ) )
17 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> y e. ( 0 ..^ N ) )
18 opeq2 
 |-  ( z = y -> <. 0 , z >. = <. 0 , y >. )
19 oveq1 
 |-  ( z = y -> ( z + 1 ) = ( y + 1 ) )
20 19 oveq1d 
 |-  ( z = y -> ( ( z + 1 ) mod N ) = ( ( y + 1 ) mod N ) )
21 20 opeq2d 
 |-  ( z = y -> <. 0 , ( ( z + 1 ) mod N ) >. = <. 0 , ( ( y + 1 ) mod N ) >. )
22 18 21 preq12d 
 |-  ( z = y -> { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } )
23 22 eqeq2d 
 |-  ( z = y -> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } ) )
24 opeq2 
 |-  ( z = y -> <. 1 , z >. = <. 1 , y >. )
25 18 24 preq12d 
 |-  ( z = y -> { <. 0 , z >. , <. 1 , z >. } = { <. 0 , y >. , <. 1 , y >. } )
26 25 eqeq2d 
 |-  ( z = y -> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } ) )
27 oveq1 
 |-  ( z = y -> ( z + K ) = ( y + K ) )
28 27 oveq1d 
 |-  ( z = y -> ( ( z + K ) mod N ) = ( ( y + K ) mod N ) )
29 28 opeq2d 
 |-  ( z = y -> <. 1 , ( ( z + K ) mod N ) >. = <. 1 , ( ( y + K ) mod N ) >. )
30 24 29 preq12d 
 |-  ( z = y -> { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } )
31 30 eqeq2d 
 |-  ( z = y -> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
32 23 26 31 3orbi123d 
 |-  ( z = y -> ( ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
33 32 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) /\ z = y ) -> ( ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
34 eqid 
 |-  { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. }
35 34 3mix1i 
 |-  ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } )
36 35 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
37 17 33 36 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
38 22 eqeq2d 
 |-  ( z = y -> ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } ) )
39 25 eqeq2d 
 |-  ( z = y -> ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 1 , y >. } ) )
40 30 eqeq2d 
 |-  ( z = y -> ( { <. 0 , y >. , <. 1 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 0 , y >. , <. 1 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
41 38 39 40 3orbi123d 
 |-  ( z = y -> ( ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
42 41 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) /\ z = y ) -> ( ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
43 eqid 
 |-  { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 1 , y >. }
44 43 3mix2i 
 |-  ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } )
45 44 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , y >. , <. 1 , y >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) )
46 17 42 45 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
47 elfzo0l 
 |-  ( y e. ( 0 ..^ N ) -> ( y = 0 \/ y e. ( 1 ..^ N ) ) )
48 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
49 48 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y = 0 ) -> N e. NN )
50 fzo0end 
 |-  ( N e. NN -> ( N - 1 ) e. ( 0 ..^ N ) )
51 49 50 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y = 0 ) -> ( N - 1 ) e. ( 0 ..^ N ) )
52 opeq2 
 |-  ( y = 0 -> <. 0 , y >. = <. 0 , 0 >. )
53 oveq1 
 |-  ( y = 0 -> ( y - 1 ) = ( 0 - 1 ) )
54 53 oveq1d 
 |-  ( y = 0 -> ( ( y - 1 ) mod N ) = ( ( 0 - 1 ) mod N ) )
55 54 opeq2d 
 |-  ( y = 0 -> <. 0 , ( ( y - 1 ) mod N ) >. = <. 0 , ( ( 0 - 1 ) mod N ) >. )
56 52 55 preq12d 
 |-  ( y = 0 -> { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } )
57 opeq2 
 |-  ( z = ( N - 1 ) -> <. 0 , z >. = <. 0 , ( N - 1 ) >. )
58 oveq1 
 |-  ( z = ( N - 1 ) -> ( z + 1 ) = ( ( N - 1 ) + 1 ) )
59 58 oveq1d 
 |-  ( z = ( N - 1 ) -> ( ( z + 1 ) mod N ) = ( ( ( N - 1 ) + 1 ) mod N ) )
60 59 opeq2d 
 |-  ( z = ( N - 1 ) -> <. 0 , ( ( z + 1 ) mod N ) >. = <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. )
61 57 60 preq12d 
 |-  ( z = ( N - 1 ) -> { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. } )
62 56 61 eqeqan12d 
 |-  ( ( y = 0 /\ z = ( N - 1 ) ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. } ) )
63 opeq2 
 |-  ( z = ( N - 1 ) -> <. 1 , z >. = <. 1 , ( N - 1 ) >. )
64 57 63 preq12d 
 |-  ( z = ( N - 1 ) -> { <. 0 , z >. , <. 1 , z >. } = { <. 0 , ( N - 1 ) >. , <. 1 , ( N - 1 ) >. } )
65 56 64 eqeqan12d 
 |-  ( ( y = 0 /\ z = ( N - 1 ) ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 1 , ( N - 1 ) >. } ) )
66 oveq1 
 |-  ( z = ( N - 1 ) -> ( z + K ) = ( ( N - 1 ) + K ) )
67 66 oveq1d 
 |-  ( z = ( N - 1 ) -> ( ( z + K ) mod N ) = ( ( ( N - 1 ) + K ) mod N ) )
68 67 opeq2d 
 |-  ( z = ( N - 1 ) -> <. 1 , ( ( z + K ) mod N ) >. = <. 1 , ( ( ( N - 1 ) + K ) mod N ) >. )
69 63 68 preq12d 
 |-  ( z = ( N - 1 ) -> { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } = { <. 1 , ( N - 1 ) >. , <. 1 , ( ( ( N - 1 ) + K ) mod N ) >. } )
70 56 69 eqeqan12d 
 |-  ( ( y = 0 /\ z = ( N - 1 ) ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 1 , ( N - 1 ) >. , <. 1 , ( ( ( N - 1 ) + K ) mod N ) >. } ) )
71 62 65 70 3orbi123d 
 |-  ( ( y = 0 /\ z = ( N - 1 ) ) -> ( ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 1 , ( N - 1 ) >. } \/ { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 1 , ( N - 1 ) >. , <. 1 , ( ( ( N - 1 ) + K ) mod N ) >. } ) ) )
72 71 adantll 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y = 0 ) /\ z = ( N - 1 ) ) -> ( ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 1 , ( N - 1 ) >. } \/ { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 1 , ( N - 1 ) >. , <. 1 , ( ( ( N - 1 ) + K ) mod N ) >. } ) ) )
73 nncn 
 |-  ( N e. NN -> N e. CC )
74 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
75 48 73 74 3syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 1 ) + 1 ) = N )
76 75 oveq1d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( ( N - 1 ) + 1 ) mod N ) = ( N mod N ) )
77 nnrp 
 |-  ( N e. NN -> N e. RR+ )
78 modid0 
 |-  ( N e. RR+ -> ( N mod N ) = 0 )
79 48 77 78 3syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N mod N ) = 0 )
80 76 79 eqtr2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 = ( ( ( N - 1 ) + 1 ) mod N ) )
81 80 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 0 >. = <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. )
82 df-neg 
 |-  -u 1 = ( 0 - 1 )
83 82 eqcomi 
 |-  ( 0 - 1 ) = -u 1
84 83 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 0 - 1 ) = -u 1 )
85 84 oveq1d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( 0 - 1 ) mod N ) = ( -u 1 mod N ) )
86 m1modnnsub1 
 |-  ( N e. NN -> ( -u 1 mod N ) = ( N - 1 ) )
87 48 86 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( -u 1 mod N ) = ( N - 1 ) )
88 85 87 eqtrd 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( 0 - 1 ) mod N ) = ( N - 1 ) )
89 88 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , ( ( 0 - 1 ) mod N ) >. = <. 0 , ( N - 1 ) >. )
90 81 89 preq12d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. , <. 0 , ( N - 1 ) >. } )
91 90 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y = 0 ) -> { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. , <. 0 , ( N - 1 ) >. } )
92 prcom 
 |-  { <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. , <. 0 , ( N - 1 ) >. } = { <. 0 , ( N - 1 ) >. , <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. }
93 91 92 eqtrdi 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y = 0 ) -> { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. } )
94 93 3mix1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y = 0 ) -> ( { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 0 , ( ( ( N - 1 ) + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 0 , ( N - 1 ) >. , <. 1 , ( N - 1 ) >. } \/ { <. 0 , 0 >. , <. 0 , ( ( 0 - 1 ) mod N ) >. } = { <. 1 , ( N - 1 ) >. , <. 1 , ( ( ( N - 1 ) + K ) mod N ) >. } ) )
95 51 72 94 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y = 0 ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
96 95 expcom 
 |-  ( y = 0 -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
97 elfzofz 
 |-  ( y e. ( 1 ..^ N ) -> y e. ( 1 ... N ) )
98 fz1fzo0m1 
 |-  ( y e. ( 1 ... N ) -> ( y - 1 ) e. ( 0 ..^ N ) )
99 97 98 syl 
 |-  ( y e. ( 1 ..^ N ) -> ( y - 1 ) e. ( 0 ..^ N ) )
100 99 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> ( y - 1 ) e. ( 0 ..^ N ) )
101 opeq2 
 |-  ( z = ( y - 1 ) -> <. 0 , z >. = <. 0 , ( y - 1 ) >. )
102 oveq1 
 |-  ( z = ( y - 1 ) -> ( z + 1 ) = ( ( y - 1 ) + 1 ) )
103 102 oveq1d 
 |-  ( z = ( y - 1 ) -> ( ( z + 1 ) mod N ) = ( ( ( y - 1 ) + 1 ) mod N ) )
104 103 opeq2d 
 |-  ( z = ( y - 1 ) -> <. 0 , ( ( z + 1 ) mod N ) >. = <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. )
105 101 104 preq12d 
 |-  ( z = ( y - 1 ) -> { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. } )
106 105 eqeq2d 
 |-  ( z = ( y - 1 ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } <-> { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. } ) )
107 opeq2 
 |-  ( z = ( y - 1 ) -> <. 1 , z >. = <. 1 , ( y - 1 ) >. )
108 101 107 preq12d 
 |-  ( z = ( y - 1 ) -> { <. 0 , z >. , <. 1 , z >. } = { <. 0 , ( y - 1 ) >. , <. 1 , ( y - 1 ) >. } )
109 108 eqeq2d 
 |-  ( z = ( y - 1 ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } <-> { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 1 , ( y - 1 ) >. } ) )
110 oveq1 
 |-  ( z = ( y - 1 ) -> ( z + K ) = ( ( y - 1 ) + K ) )
111 110 oveq1d 
 |-  ( z = ( y - 1 ) -> ( ( z + K ) mod N ) = ( ( ( y - 1 ) + K ) mod N ) )
112 111 opeq2d 
 |-  ( z = ( y - 1 ) -> <. 1 , ( ( z + K ) mod N ) >. = <. 1 , ( ( ( y - 1 ) + K ) mod N ) >. )
113 107 112 preq12d 
 |-  ( z = ( y - 1 ) -> { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } = { <. 1 , ( y - 1 ) >. , <. 1 , ( ( ( y - 1 ) + K ) mod N ) >. } )
114 113 eqeq2d 
 |-  ( z = ( y - 1 ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } <-> { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , ( y - 1 ) >. , <. 1 , ( ( ( y - 1 ) + K ) mod N ) >. } ) )
115 106 109 114 3orbi123d 
 |-  ( z = ( y - 1 ) -> ( ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 1 , ( y - 1 ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , ( y - 1 ) >. , <. 1 , ( ( ( y - 1 ) + K ) mod N ) >. } ) ) )
116 115 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) /\ z = ( y - 1 ) ) -> ( ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) <-> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 1 , ( y - 1 ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , ( y - 1 ) >. , <. 1 , ( ( ( y - 1 ) + K ) mod N ) >. } ) ) )
117 elfzoelz 
 |-  ( y e. ( 1 ..^ N ) -> y e. ZZ )
118 zcn 
 |-  ( y e. ZZ -> y e. CC )
119 npcan1 
 |-  ( y e. CC -> ( ( y - 1 ) + 1 ) = y )
120 117 118 119 3syl 
 |-  ( y e. ( 1 ..^ N ) -> ( ( y - 1 ) + 1 ) = y )
121 120 oveq1d 
 |-  ( y e. ( 1 ..^ N ) -> ( ( ( y - 1 ) + 1 ) mod N ) = ( y mod N ) )
122 elfzo1 
 |-  ( y e. ( 1 ..^ N ) <-> ( y e. NN /\ N e. NN /\ y < N ) )
123 nnre 
 |-  ( y e. NN -> y e. RR )
124 123 77 anim12i 
 |-  ( ( y e. NN /\ N e. NN ) -> ( y e. RR /\ N e. RR+ ) )
125 124 3adant3 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( y e. RR /\ N e. RR+ ) )
126 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
127 126 nn0ge0d 
 |-  ( y e. NN -> 0 <_ y )
128 127 anim1i 
 |-  ( ( y e. NN /\ y < N ) -> ( 0 <_ y /\ y < N ) )
129 128 3adant2 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( 0 <_ y /\ y < N ) )
130 125 129 jca 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( ( y e. RR /\ N e. RR+ ) /\ ( 0 <_ y /\ y < N ) ) )
131 122 130 sylbi 
 |-  ( y e. ( 1 ..^ N ) -> ( ( y e. RR /\ N e. RR+ ) /\ ( 0 <_ y /\ y < N ) ) )
132 modid 
 |-  ( ( ( y e. RR /\ N e. RR+ ) /\ ( 0 <_ y /\ y < N ) ) -> ( y mod N ) = y )
133 131 132 syl 
 |-  ( y e. ( 1 ..^ N ) -> ( y mod N ) = y )
134 121 133 eqtrd 
 |-  ( y e. ( 1 ..^ N ) -> ( ( ( y - 1 ) + 1 ) mod N ) = y )
135 134 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> ( ( ( y - 1 ) + 1 ) mod N ) = y )
136 135 eqcomd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> y = ( ( ( y - 1 ) + 1 ) mod N ) )
137 136 opeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> <. 0 , y >. = <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. )
138 1red 
 |-  ( y e. NN -> 1 e. RR )
139 123 138 resubcld 
 |-  ( y e. NN -> ( y - 1 ) e. RR )
140 139 77 anim12i 
 |-  ( ( y e. NN /\ N e. NN ) -> ( ( y - 1 ) e. RR /\ N e. RR+ ) )
141 140 3adant3 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( ( y - 1 ) e. RR /\ N e. RR+ ) )
142 nnm1ge0 
 |-  ( y e. NN -> 0 <_ ( y - 1 ) )
143 142 3ad2ant1 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> 0 <_ ( y - 1 ) )
144 139 3ad2ant1 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( y - 1 ) e. RR )
145 123 3ad2ant1 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> y e. RR )
146 nnre 
 |-  ( N e. NN -> N e. RR )
147 146 3ad2ant2 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> N e. RR )
148 123 ltm1d 
 |-  ( y e. NN -> ( y - 1 ) < y )
149 148 3ad2ant1 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( y - 1 ) < y )
150 simp3 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> y < N )
151 144 145 147 149 150 lttrd 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( y - 1 ) < N )
152 141 143 151 jca32 
 |-  ( ( y e. NN /\ N e. NN /\ y < N ) -> ( ( ( y - 1 ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( y - 1 ) /\ ( y - 1 ) < N ) ) )
153 122 152 sylbi 
 |-  ( y e. ( 1 ..^ N ) -> ( ( ( y - 1 ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( y - 1 ) /\ ( y - 1 ) < N ) ) )
154 153 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> ( ( ( y - 1 ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( y - 1 ) /\ ( y - 1 ) < N ) ) )
155 modid 
 |-  ( ( ( ( y - 1 ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( y - 1 ) /\ ( y - 1 ) < N ) ) -> ( ( y - 1 ) mod N ) = ( y - 1 ) )
156 154 155 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> ( ( y - 1 ) mod N ) = ( y - 1 ) )
157 156 opeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> <. 0 , ( ( y - 1 ) mod N ) >. = <. 0 , ( y - 1 ) >. )
158 137 157 preq12d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. , <. 0 , ( y - 1 ) >. } )
159 prcom 
 |-  { <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. , <. 0 , ( y - 1 ) >. } = { <. 0 , ( y - 1 ) >. , <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. }
160 158 159 eqtrdi 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. } )
161 160 3mix1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 0 , ( ( ( y - 1 ) + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , ( y - 1 ) >. , <. 1 , ( y - 1 ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , ( y - 1 ) >. , <. 1 , ( ( ( y - 1 ) + K ) mod N ) >. } ) )
162 100 116 161 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 1 ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
163 162 expcom 
 |-  ( y e. ( 1 ..^ N ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
164 96 163 jaoi 
 |-  ( ( y = 0 \/ y e. ( 1 ..^ N ) ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
165 47 164 syl 
 |-  ( y e. ( 0 ..^ N ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
166 165 impcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) )
167 5 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } e. E <-> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
168 5 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 0 , y >. , <. 1 , y >. } e. E <-> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
169 5 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } e. E <-> E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) )
170 167 168 169 3anbi123d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } e. E /\ { <. 0 , y >. , <. 1 , y >. } e. E /\ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } e. E ) <-> ( E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) ) )
171 170 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } e. E /\ { <. 0 , y >. , <. 1 , y >. } e. E /\ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } e. E ) <-> ( E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 1 , y >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) /\ E. z e. ( 0 ..^ N ) ( { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 0 , ( ( z + 1 ) mod N ) >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 0 , z >. , <. 1 , z >. } \/ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } = { <. 1 , z >. , <. 1 , ( ( z + K ) mod N ) >. } ) ) ) )
172 37 46 166 171 mpbir3and 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ y e. ( 0 ..^ N ) ) -> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } e. E /\ { <. 0 , y >. , <. 1 , y >. } e. E /\ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } e. E ) )
173 172 adantrl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } e. E /\ { <. 0 , y >. , <. 1 , y >. } e. E /\ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } e. E ) )
174 id 
 |-  ( X = <. 0 , y >. -> X = <. 0 , y >. )
175 c0ex 
 |-  0 e. _V
176 175 10 op2ndd 
 |-  ( X = <. 0 , y >. -> ( 2nd ` X ) = y )
177 176 oveq1d 
 |-  ( X = <. 0 , y >. -> ( ( 2nd ` X ) + 1 ) = ( y + 1 ) )
178 177 oveq1d 
 |-  ( X = <. 0 , y >. -> ( ( ( 2nd ` X ) + 1 ) mod N ) = ( ( y + 1 ) mod N ) )
179 178 opeq2d 
 |-  ( X = <. 0 , y >. -> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. = <. 0 , ( ( y + 1 ) mod N ) >. )
180 174 179 preq12d 
 |-  ( X = <. 0 , y >. -> { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } )
181 180 eleq1d 
 |-  ( X = <. 0 , y >. -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E <-> { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } e. E ) )
182 176 opeq2d 
 |-  ( X = <. 0 , y >. -> <. 1 , ( 2nd ` X ) >. = <. 1 , y >. )
183 174 182 preq12d 
 |-  ( X = <. 0 , y >. -> { X , <. 1 , ( 2nd ` X ) >. } = { <. 0 , y >. , <. 1 , y >. } )
184 183 eleq1d 
 |-  ( X = <. 0 , y >. -> ( { X , <. 1 , ( 2nd ` X ) >. } e. E <-> { <. 0 , y >. , <. 1 , y >. } e. E ) )
185 176 oveq1d 
 |-  ( X = <. 0 , y >. -> ( ( 2nd ` X ) - 1 ) = ( y - 1 ) )
186 185 oveq1d 
 |-  ( X = <. 0 , y >. -> ( ( ( 2nd ` X ) - 1 ) mod N ) = ( ( y - 1 ) mod N ) )
187 186 opeq2d 
 |-  ( X = <. 0 , y >. -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. = <. 0 , ( ( y - 1 ) mod N ) >. )
188 174 187 preq12d 
 |-  ( X = <. 0 , y >. -> { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } = { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } )
189 188 eleq1d 
 |-  ( X = <. 0 , y >. -> ( { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E <-> { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } e. E ) )
190 181 184 189 3anbi123d 
 |-  ( X = <. 0 , y >. -> ( ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) <-> ( { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } e. E /\ { <. 0 , y >. , <. 1 , y >. } e. E /\ { <. 0 , y >. , <. 0 , ( ( y - 1 ) mod N ) >. } e. E ) ) )
191 173 190 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( X = <. 0 , y >. -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) )
192 191 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ x = 0 ) -> ( X = <. 0 , y >. -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) )
193 16 192 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ x = 0 ) -> ( X = <. x , y >. -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) )
194 193 impancom 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ X = <. x , y >. ) -> ( x = 0 -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) )
195 13 194 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) /\ X = <. x , y >. ) -> ( ( 1st ` X ) = 0 -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) )
196 195 ex 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( X = <. x , y >. -> ( ( 1st ` X ) = 0 -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) ) )
197 196 rexlimdvva 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( E. x e. { 0 , 1 } E. y e. ( 0 ..^ N ) X = <. x , y >. -> ( ( 1st ` X ) = 0 -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) ) )
198 6 197 sylbid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V -> ( ( 1st ` X ) = 0 -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) ) ) )
199 198 imp32 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( { X , <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. } e. E /\ { X , <. 1 , ( 2nd ` X ) >. } e. E /\ { X , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } e. E ) )