Metamath Proof Explorer

Theorem gpgedg2ov

Description: The edges of the generalized Petersen graph GPG(N,K) between two outside vertices. (Contributed by AV, 15-Nov-2025)

Ref Expression
Hypotheses gpgedgiov.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgedgiov.i 
|- I = ( 0 ..^ N )
gpgedgiov.g 
|- G = ( N gPetersenGr K )
gpgedgiov.e 
|- E = ( Edg ` G )
Assertion gpgedg2ov 
|- ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 gpgedgiov.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgedgiov.i 
 |-  I = ( 0 ..^ N )
3 gpgedgiov.g 
 |-  G = ( N gPetersenGr K )
4 gpgedgiov.e 
 |-  E = ( Edg ` G )
5 prcom 
 |-  { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } = { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. }
6 5 eleq1i 
 |-  ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E <-> { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E )
7 uzuzle35 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. ( ZZ>= ` 3 ) )
8 7 anim1i 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
9 8 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
10 9 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
11 c0ex 
 |-  0 e. _V
12 11 a1i 
 |-  ( Y e. I -> 0 e. _V )
13 12 anim1i 
 |-  ( ( Y e. I /\ X e. I ) -> ( 0 e. _V /\ X e. I ) )
14 13 ancoms 
 |-  ( ( X e. I /\ Y e. I ) -> ( 0 e. _V /\ X e. I ) )
15 op1stg 
 |-  ( ( 0 e. _V /\ X e. I ) -> ( 1st ` <. 0 , X >. ) = 0 )
16 14 15 syl 
 |-  ( ( X e. I /\ Y e. I ) -> ( 1st ` <. 0 , X >. ) = 0 )
17 16 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( 1st ` <. 0 , X >. ) = 0 )
18 17 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E ) -> ( 1st ` <. 0 , X >. ) = 0 )
19 simpr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E ) -> { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E )
20 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
21 1 3 20 4 gpgvtxedg0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` <. 0 , X >. ) = 0 /\ { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) )
22 10 18 19 21 syl3anc 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) )
23 22 ex 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , X >. , <. 0 , ( ( Y - 1 ) mod N ) >. } e. E -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) ) )
24 6 23 biimtrid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) ) )
25 9 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
26 17 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) -> ( 1st ` <. 0 , X >. ) = 0 )
27 simpr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) -> { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E )
28 1 3 20 4 gpgvtxedg0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` <. 0 , X >. ) = 0 /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) )
29 25 26 27 28 syl3anc 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) )
30 29 ex 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) ) )
31 ovex 
 |-  ( ( Y + 1 ) mod N ) e. _V
32 11 31 opth 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. <-> ( 0 = 0 /\ ( ( Y + 1 ) mod N ) = ( ( X + 1 ) mod N ) ) )
33 7 adantr 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) -> N e. ( ZZ>= ` 3 ) )
34 33 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> N e. ( ZZ>= ` 3 ) )
35 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( X e. I /\ Y e. I ) )
36 35 ancomd 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( Y e. I /\ X e. I ) )
37 1zzd 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> 1 e. ZZ )
38 2 modaddid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( Y e. I /\ X e. I ) /\ 1 e. ZZ ) -> ( ( ( Y + 1 ) mod N ) = ( ( X + 1 ) mod N ) <-> Y = X ) )
39 34 36 37 38 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( Y + 1 ) mod N ) = ( ( X + 1 ) mod N ) <-> Y = X ) )
40 39 biimpa 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ ( ( Y + 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> Y = X )
41 40 eqcomd 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ ( ( Y + 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> X = Y )
42 41 ex 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( Y + 1 ) mod N ) = ( ( X + 1 ) mod N ) -> X = Y ) )
43 42 adantld 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( 0 = 0 /\ ( ( Y + 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> X = Y ) )
44 32 43 biimtrid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) )
45 44 imp 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. ) -> X = Y )
46 45 a1d 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) )
47 46 ex 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) )
48 11 31 opth 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. <-> ( 0 = 1 /\ ( ( Y + 1 ) mod N ) = X ) )
49 0ne1 
 |-  0 =/= 1
50 eqneqall 
 |-  ( 0 = 1 -> ( 0 =/= 1 -> ( ( ( Y + 1 ) mod N ) = X -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) ) ) )
51 49 50 mpi 
 |-  ( 0 = 1 -> ( ( ( Y + 1 ) mod N ) = X -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) ) )
52 51 imp 
 |-  ( ( 0 = 1 /\ ( ( Y + 1 ) mod N ) = X ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) )
53 52 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( 0 = 1 /\ ( ( Y + 1 ) mod N ) = X ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) ) )
54 48 53 biimtrid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) ) )
55 54 imp 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) )
56 eqeq2 
 |-  ( <. 1 , X >. = <. 0 , ( ( Y + 1 ) mod N ) >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. ) )
57 56 eqcoms 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. ) )
58 57 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. ) )
59 ovex 
 |-  ( ( Y - 1 ) mod N ) e. _V
60 11 59 opth 
 |-  ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. <-> ( 0 = 0 /\ ( ( Y - 1 ) mod N ) = ( ( Y + 1 ) mod N ) ) )
61 simpr 
 |-  ( ( X e. I /\ Y e. I ) -> Y e. I )
62 2 modm1nep1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I ) -> ( ( Y - 1 ) mod N ) =/= ( ( Y + 1 ) mod N ) )
63 33 61 62 syl2an 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( Y - 1 ) mod N ) =/= ( ( Y + 1 ) mod N ) )
64 eqneqall 
 |-  ( ( ( Y - 1 ) mod N ) = ( ( Y + 1 ) mod N ) -> ( ( ( Y - 1 ) mod N ) =/= ( ( Y + 1 ) mod N ) -> X = Y ) )
65 64 com12 
 |-  ( ( ( Y - 1 ) mod N ) =/= ( ( Y + 1 ) mod N ) -> ( ( ( Y - 1 ) mod N ) = ( ( Y + 1 ) mod N ) -> X = Y ) )
66 63 65 syl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( Y - 1 ) mod N ) = ( ( Y + 1 ) mod N ) -> X = Y ) )
67 66 adantld 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( 0 = 0 /\ ( ( Y - 1 ) mod N ) = ( ( Y + 1 ) mod N ) ) -> X = Y ) )
68 60 67 biimtrid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. -> X = Y ) )
69 68 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. -> X = Y ) )
70 58 69 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. -> X = Y ) )
71 49 orci 
 |-  ( 0 =/= 1 \/ ( ( Y + 1 ) mod N ) =/= X )
72 11 31 opthne 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. =/= <. 1 , X >. <-> ( 0 =/= 1 \/ ( ( Y + 1 ) mod N ) =/= X ) )
73 71 72 mpbir 
 |-  <. 0 , ( ( Y + 1 ) mod N ) >. =/= <. 1 , X >.
74 73 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> <. 0 , ( ( Y + 1 ) mod N ) >. =/= <. 1 , X >. )
75 eqneqall 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. -> ( <. 0 , ( ( Y + 1 ) mod N ) >. =/= <. 1 , X >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> X = Y ) ) )
76 75 com12 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. =/= <. 1 , X >. -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> X = Y ) ) )
77 74 76 syl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> X = Y ) ) )
78 77 imp 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> X = Y ) )
79 55 70 78 3jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) )
80 79 ex 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) )
81 11 31 opth 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. <-> ( 0 = 0 /\ ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) ) )
82 11 59 opth 
 |-  ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. <-> ( 0 = 0 /\ ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) ) )
83 simpll 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> N e. ( ZZ>= ` 5 ) )
84 simprl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> X e. I )
85 simprr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> Y e. I )
86 2 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 ) ) )
87 83 84 85 86 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) -> ( ( Y + 1 ) mod N ) =/= ( ( X - 1 ) mod N ) ) )
88 eqneqall 
 |-  ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) -> ( ( ( Y + 1 ) mod N ) =/= ( ( X - 1 ) mod N ) -> X = Y ) )
89 88 com12 
 |-  ( ( ( Y + 1 ) mod N ) =/= ( ( X - 1 ) mod N ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) -> X = Y ) )
90 89 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( Y + 1 ) mod N ) =/= ( ( X - 1 ) mod N ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) -> X = Y ) ) )
91 87 90 syld 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) -> X = Y ) ) )
92 91 adantld 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( 0 = 0 /\ ( ( Y - 1 ) mod N ) = ( ( X + 1 ) mod N ) ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) -> X = Y ) ) )
93 82 92 biimtrid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) -> X = Y ) ) )
94 93 com23 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) ) )
95 94 adantld 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( 0 = 0 /\ ( ( Y + 1 ) mod N ) = ( ( X - 1 ) mod N ) ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) ) )
96 81 95 biimtrid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) ) )
97 96 imp 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) )
98 49 orci 
 |-  ( 0 =/= 1 \/ ( ( Y - 1 ) mod N ) =/= X )
99 11 59 opthne 
 |-  ( <. 0 , ( ( Y - 1 ) mod N ) >. =/= <. 1 , X >. <-> ( 0 =/= 1 \/ ( ( Y - 1 ) mod N ) =/= X ) )
100 98 99 mpbir 
 |-  <. 0 , ( ( Y - 1 ) mod N ) >. =/= <. 1 , X >.
101 eqneqall 
 |-  ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. =/= <. 1 , X >. -> X = Y ) )
102 100 101 mpi 
 |-  ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. -> X = Y )
103 102 a1i 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. -> X = Y ) )
104 eqeq2 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. ) )
105 104 eqcoms 
 |-  ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. ) )
106 105 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. ) )
107 68 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. -> X = Y ) )
108 106 107 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> X = Y ) )
109 97 103 108 3jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) )
110 109 ex 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) )
111 47 80 110 3jaod 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) )
112 op2ndg 
 |-  ( ( 0 e. _V /\ X e. I ) -> ( 2nd ` <. 0 , X >. ) = X )
113 11 112 mpan 
 |-  ( X e. I -> ( 2nd ` <. 0 , X >. ) = X )
114 113 adantr 
 |-  ( ( X e. I /\ Y e. I ) -> ( 2nd ` <. 0 , X >. ) = X )
115 114 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( 2nd ` <. 0 , X >. ) = X )
116 oveq1 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( 2nd ` <. 0 , X >. ) + 1 ) = ( X + 1 ) )
117 116 oveq1d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) = ( ( X + 1 ) mod N ) )
118 117 opeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. )
119 118 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. <-> <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. ) )
120 opeq2 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> <. 1 , ( 2nd ` <. 0 , X >. ) >. = <. 1 , X >. )
121 120 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. <-> <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. ) )
122 oveq1 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( 2nd ` <. 0 , X >. ) - 1 ) = ( X - 1 ) )
123 122 oveq1d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) = ( ( X - 1 ) mod N ) )
124 123 opeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. )
125 124 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. <-> <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) )
126 119 121 125 3orbi123d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) <-> ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) ) )
127 118 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. ) )
128 120 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. ) )
129 124 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. <-> <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) )
130 127 128 129 3orbi123d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) <-> ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) ) )
131 130 imbi1d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) <-> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) )
132 126 131 imbi12d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) ) <-> ( ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) ) )
133 115 132 syl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) ) <-> ( ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , X >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) ) )
134 111 133 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) ) )
135 30 134 syld 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) ) )
136 135 com23 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 0 , ( ( Y - 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> ( { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E -> X = Y ) ) )
137 24 136 syld 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E -> ( { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E -> X = Y ) ) )
138 137 impd 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) -> X = Y ) )
139 eqid 
 |-  0 = 0
140 139 orci 
 |-  ( 0 = 0 \/ 0 = 1 )
141 61 140 jctil 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( 0 = 0 \/ 0 = 1 ) /\ Y e. I ) )
142 141 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( 0 = 0 \/ 0 = 1 ) /\ Y e. I ) )
143 2 1 3 20 opgpgvtx 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( <. 0 , Y >. e. ( Vtx ` G ) <-> ( ( 0 = 0 \/ 0 = 1 ) /\ Y e. I ) ) )
144 8 143 syl 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) -> ( <. 0 , Y >. e. ( Vtx ` G ) <-> ( ( 0 = 0 \/ 0 = 1 ) /\ Y e. I ) ) )
145 144 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( <. 0 , Y >. e. ( Vtx ` G ) <-> ( ( 0 = 0 \/ 0 = 1 ) /\ Y e. I ) ) )
146 142 145 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> <. 0 , Y >. e. ( Vtx ` G ) )
147 11 a1i 
 |-  ( X e. I -> 0 e. _V )
148 op1stg 
 |-  ( ( 0 e. _V /\ Y e. I ) -> ( 1st ` <. 0 , Y >. ) = 0 )
149 147 148 sylan 
 |-  ( ( X e. I /\ Y e. I ) -> ( 1st ` <. 0 , Y >. ) = 0 )
150 149 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( 1st ` <. 0 , Y >. ) = 0 )
151 1 3 20 4 gpgedgvtx0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( <. 0 , Y >. e. ( Vtx ` G ) /\ ( 1st ` <. 0 , Y >. ) = 0 ) ) -> ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 1 , ( 2nd ` <. 0 , Y >. ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E ) )
152 9 146 150 151 syl12anc 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 1 , ( 2nd ` <. 0 , Y >. ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E ) )
153 op2ndg 
 |-  ( ( 0 e. _V /\ Y e. I ) -> ( 2nd ` <. 0 , Y >. ) = Y )
154 11 153 mpan 
 |-  ( Y e. I -> ( 2nd ` <. 0 , Y >. ) = Y )
155 oveq1 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> ( ( 2nd ` <. 0 , Y >. ) - 1 ) = ( Y - 1 ) )
156 155 oveq1d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) = ( ( Y - 1 ) mod N ) )
157 156 opeq2d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. = <. 0 , ( ( Y - 1 ) mod N ) >. )
158 157 preq2d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } = { <. 0 , Y >. , <. 0 , ( ( Y - 1 ) mod N ) >. } )
159 prcom 
 |-  { <. 0 , Y >. , <. 0 , ( ( Y - 1 ) mod N ) >. } = { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. }
160 158 159 eqtrdi 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } = { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } )
161 160 eleq1d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E <-> { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E ) )
162 oveq1 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> ( ( 2nd ` <. 0 , Y >. ) + 1 ) = ( Y + 1 ) )
163 162 oveq1d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) = ( ( Y + 1 ) mod N ) )
164 163 opeq2d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. )
165 164 preq2d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } = { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } )
166 165 eleq1d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E <-> { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) )
167 161 166 anbi12d 
 |-  ( ( 2nd ` <. 0 , Y >. ) = Y -> ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E ) <-> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
168 154 167 syl 
 |-  ( Y e. I -> ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E ) <-> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
169 168 biimpcd 
 |-  ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E ) -> ( Y e. I -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
170 169 ancoms 
 |-  ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E ) -> ( Y e. I -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
171 170 3adant2 
 |-  ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 1 , ( 2nd ` <. 0 , Y >. ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E ) -> ( Y e. I -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
172 171 com12 
 |-  ( Y e. I -> ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 1 , ( 2nd ` <. 0 , Y >. ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E ) -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
173 172 adantl 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 1 , ( 2nd ` <. 0 , Y >. ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E ) -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
174 173 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) + 1 ) mod N ) >. } e. E /\ { <. 0 , Y >. , <. 1 , ( 2nd ` <. 0 , Y >. ) >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( ( 2nd ` <. 0 , Y >. ) - 1 ) mod N ) >. } e. E ) -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
175 152 174 mpd 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) )
176 opeq2 
 |-  ( X = Y -> <. 0 , X >. = <. 0 , Y >. )
177 176 preq2d 
 |-  ( X = Y -> { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } = { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } )
178 177 eleq1d 
 |-  ( X = Y -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E <-> { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E ) )
179 176 preq1d 
 |-  ( X = Y -> { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } = { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } )
180 179 eleq1d 
 |-  ( X = Y -> ( { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E <-> { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) )
181 178 180 anbi12d 
 |-  ( X = Y -> ( ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) <-> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , Y >. } e. E /\ { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
182 175 181 syl5ibrcom 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( X = Y -> ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) ) )
183 138 182 impbid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( { <. 0 , ( ( Y - 1 ) mod N ) >. , <. 0 , X >. } e. E /\ { <. 0 , X >. , <. 0 , ( ( Y + 1 ) mod N ) >. } e. E ) <-> X = Y ) )