Metamath Proof Explorer

Theorem gpgedg2iv

Description: The edges of the generalized Petersen graph GPG(N,K) between two inside vertices. (Contributed by AV, 20-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 gpgedg2iv 
|- ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) 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 
 |-  { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } = { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. }
6 5 eleq1i 
 |-  ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E <-> { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E )
7 uzuzle35 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. ( ZZ>= ` 3 ) )
8 simpl 
 |-  ( ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) -> K e. J )
9 7 8 anim12i 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
10 9 3adant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
11 10 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
12 1ex 
 |-  1 e. _V
13 12 a1i 
 |-  ( Y e. I -> 1 e. _V )
14 13 anim1i 
 |-  ( ( Y e. I /\ X e. I ) -> ( 1 e. _V /\ X e. I ) )
15 14 ancoms 
 |-  ( ( X e. I /\ Y e. I ) -> ( 1 e. _V /\ X e. I ) )
16 op1stg 
 |-  ( ( 1 e. _V /\ X e. I ) -> ( 1st ` <. 1 , X >. ) = 1 )
17 15 16 syl 
 |-  ( ( X e. I /\ Y e. I ) -> ( 1st ` <. 1 , X >. ) = 1 )
18 17 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( 1st ` <. 1 , X >. ) = 1 )
19 18 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E ) -> ( 1st ` <. 1 , X >. ) = 1 )
20 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E ) -> { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E )
21 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
22 1 3 21 4 gpgvtxedg1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` <. 1 , X >. ) = 1 /\ { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) )
23 11 19 20 22 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) )
24 23 ex 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( { <. 1 , X >. , <. 1 , ( ( Y - K ) mod N ) >. } e. E -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) ) )
25 6 24 biimtrid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) ) )
26 10 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
27 18 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) -> ( 1st ` <. 1 , X >. ) = 1 )
28 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) -> { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E )
29 1 3 21 4 gpgvtxedg1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` <. 1 , X >. ) = 1 /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) )
30 26 27 28 29 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) )
31 30 ex 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) ) )
32 ovex 
 |-  ( ( Y + K ) mod N ) e. _V
33 12 32 opth 
 |-  ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. <-> ( 1 = 1 /\ ( ( Y + K ) mod N ) = ( ( X + K ) mod N ) ) )
34 7 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> N e. ( ZZ>= ` 3 ) )
35 simp2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( X e. I /\ Y e. I ) )
36 35 ancomd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( Y e. I /\ X e. I ) )
37 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
38 37 1 eleq2s 
 |-  ( K e. J -> K e. ZZ )
39 38 adantr 
 |-  ( ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) -> K e. ZZ )
40 39 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> K e. ZZ )
41 2 modaddid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( Y e. I /\ X e. I ) /\ K e. ZZ ) -> ( ( ( Y + K ) mod N ) = ( ( X + K ) mod N ) <-> Y = X ) )
42 34 36 40 41 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( ( Y + K ) mod N ) = ( ( X + K ) mod N ) <-> Y = X ) )
43 42 biimpa 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ ( ( Y + K ) mod N ) = ( ( X + K ) mod N ) ) -> Y = X )
44 43 eqcomd 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ ( ( Y + K ) mod N ) = ( ( X + K ) mod N ) ) -> X = Y )
45 44 ex 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( ( Y + K ) mod N ) = ( ( X + K ) mod N ) -> X = Y ) )
46 45 adantld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( 1 = 1 /\ ( ( Y + K ) mod N ) = ( ( X + K ) mod N ) ) -> X = Y ) )
47 33 46 biimtrid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) )
48 47 a1dd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) ) )
49 12 32 opth 
 |-  ( <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. <-> ( 1 = 0 /\ ( ( Y + K ) mod N ) = X ) )
50 49 a1i 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. <-> ( 1 = 0 /\ ( ( Y + K ) mod N ) = X ) ) )
51 ax-1ne0 
 |-  1 =/= 0
52 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( ( ( Y + K ) mod N ) = X -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) ) ) )
53 51 52 mpi 
 |-  ( 1 = 0 -> ( ( ( Y + K ) mod N ) = X -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) ) )
54 53 imp 
 |-  ( ( 1 = 0 /\ ( ( Y + K ) mod N ) = X ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) )
55 50 54 biimtrdi 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) ) )
56 55 imp 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) )
57 ovex 
 |-  ( ( Y - K ) mod N ) e. _V
58 12 57 opth 
 |-  ( <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. <-> ( 1 = 0 /\ ( ( Y - K ) mod N ) = X ) )
59 58 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. <-> ( 1 = 0 /\ ( ( Y - K ) mod N ) = X ) ) )
60 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( ( ( Y - K ) mod N ) = X -> X = Y ) ) )
61 51 60 mpi 
 |-  ( 1 = 0 -> ( ( ( Y - K ) mod N ) = X -> X = Y ) )
62 61 imp 
 |-  ( ( 1 = 0 /\ ( ( Y - K ) mod N ) = X ) -> X = Y )
63 59 62 biimtrdi 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. -> X = Y ) )
64 51 orci 
 |-  ( 1 =/= 0 \/ ( ( Y + K ) mod N ) =/= X )
65 12 32 opthne 
 |-  ( <. 1 , ( ( Y + K ) mod N ) >. =/= <. 0 , X >. <-> ( 1 =/= 0 \/ ( ( Y + K ) mod N ) =/= X ) )
66 64 65 mpbir 
 |-  <. 1 , ( ( Y + K ) mod N ) >. =/= <. 0 , X >.
67 66 a1i 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> <. 1 , ( ( Y + K ) mod N ) >. =/= <. 0 , X >. )
68 eqneqall 
 |-  ( <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. -> ( <. 1 , ( ( Y + K ) mod N ) >. =/= <. 0 , X >. -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. -> X = Y ) ) )
69 67 68 mpan9 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. -> X = Y ) )
70 56 63 69 3jaod 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) )
71 70 ex 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) ) )
72 12 32 opth 
 |-  ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. <-> ( 1 = 1 /\ ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) )
73 12 57 opth 
 |-  ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. <-> ( 1 = 1 /\ ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) ) )
74 eluz3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
75 7 74 syl 
 |-  ( N e. ( ZZ>= ` 5 ) -> N e. NN )
76 75 adantr 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) -> N e. NN )
77 76 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) -> N e. NN )
78 elfzoelz 
 |-  ( X e. ( 0 ..^ N ) -> X e. ZZ )
79 78 2 eleq2s 
 |-  ( X e. I -> X e. ZZ )
80 79 ad2antrl 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) -> X e. ZZ )
81 80 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) -> X e. ZZ )
82 elfzoelz 
 |-  ( Y e. ( 0 ..^ N ) -> Y e. ZZ )
83 82 2 eleq2s 
 |-  ( Y e. I -> Y e. ZZ )
84 83 ad2antll 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) -> Y e. ZZ )
85 84 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) -> Y e. ZZ )
86 38 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) -> K e. ZZ )
87 modmkpkne 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) ) )
88 77 81 85 86 87 syl13anc 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) -> ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) ) )
89 88 imp 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) /\ ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) )
90 eqneqall 
 |-  ( ( ( 4 x. K ) mod N ) = 0 -> ( ( ( 4 x. K ) mod N ) =/= 0 -> X = Y ) )
91 89 90 biimtrdi 
 |-  ( ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) /\ ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) -> ( ( ( 4 x. K ) mod N ) =/= 0 -> X = Y ) ) )
92 91 expimpd 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) -> ( ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) /\ ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) -> ( ( ( 4 x. K ) mod N ) =/= 0 -> X = Y ) ) )
93 92 com23 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) /\ K e. J ) -> ( ( ( 4 x. K ) mod N ) =/= 0 -> ( ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) /\ ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) -> X = Y ) ) )
94 93 expimpd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) ) -> ( ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) -> ( ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) /\ ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) -> X = Y ) ) )
95 94 3impia 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) /\ ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) -> X = Y ) )
96 95 expd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) -> X = Y ) ) )
97 96 adantld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( 1 = 1 /\ ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) -> X = Y ) ) )
98 73 97 biimtrid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) -> X = Y ) ) )
99 98 com23 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) ) )
100 99 adantld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( 1 = 1 /\ ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) ) )
101 72 100 biimtrid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) ) )
102 101 imp 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. -> X = Y ) )
103 51 orci 
 |-  ( 1 =/= 0 \/ ( ( Y - K ) mod N ) =/= X )
104 12 57 opthne 
 |-  ( <. 1 , ( ( Y - K ) mod N ) >. =/= <. 0 , X >. <-> ( 1 =/= 0 \/ ( ( Y - K ) mod N ) =/= X ) )
105 103 104 mpbir 
 |-  <. 1 , ( ( Y - K ) mod N ) >. =/= <. 0 , X >.
106 eqneqall 
 |-  ( <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. -> ( <. 1 , ( ( Y - K ) mod N ) >. =/= <. 0 , X >. -> X = Y ) )
107 105 106 mpi 
 |-  ( <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. -> X = Y )
108 107 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. -> X = Y ) )
109 eqeq2 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. <-> <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. ) )
110 109 eqcoms 
 |-  ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. <-> <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. ) )
111 110 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. <-> <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. ) )
112 12 57 opth 
 |-  ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. <-> ( 1 = 1 /\ ( ( Y - K ) mod N ) = ( ( Y + K ) mod N ) ) )
113 simpr 
 |-  ( ( X e. I /\ Y e. I ) -> Y e. I )
114 1 2 modmknepk 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ Y e. I /\ K e. J ) -> ( ( Y - K ) mod N ) =/= ( ( Y + K ) mod N ) )
115 7 113 8 114 syl3an 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( Y - K ) mod N ) =/= ( ( Y + K ) mod N ) )
116 eqneqall 
 |-  ( ( ( Y - K ) mod N ) = ( ( Y + K ) mod N ) -> ( ( ( Y - K ) mod N ) =/= ( ( Y + K ) mod N ) -> X = Y ) )
117 115 116 syl5com 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( ( Y - K ) mod N ) = ( ( Y + K ) mod N ) -> X = Y ) )
118 117 adantld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( 1 = 1 /\ ( ( Y - K ) mod N ) = ( ( Y + K ) mod N ) ) -> X = Y ) )
119 112 118 biimtrid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. -> X = Y ) )
120 119 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. -> X = Y ) )
121 111 120 sylbid 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. -> X = Y ) )
122 102 108 121 3jaod 
 |-  ( ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) /\ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) )
123 122 ex 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) ) )
124 48 71 123 3jaod 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) ) )
125 op2ndg 
 |-  ( ( 1 e. _V /\ X e. I ) -> ( 2nd ` <. 1 , X >. ) = X )
126 15 125 syl 
 |-  ( ( X e. I /\ Y e. I ) -> ( 2nd ` <. 1 , X >. ) = X )
127 126 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( 2nd ` <. 1 , X >. ) = X )
128 oveq1 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( 2nd ` <. 1 , X >. ) + K ) = ( X + K ) )
129 128 oveq1d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) = ( ( X + K ) mod N ) )
130 129 opeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. )
131 130 eqeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. <-> <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. ) )
132 opeq2 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> <. 0 , ( 2nd ` <. 1 , X >. ) >. = <. 0 , X >. )
133 132 eqeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. <-> <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. ) )
134 oveq1 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( 2nd ` <. 1 , X >. ) - K ) = ( X - K ) )
135 134 oveq1d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) = ( ( X - K ) mod N ) )
136 135 opeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. )
137 136 eqeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. <-> <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) )
138 131 133 137 3orbi123d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) <-> ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) ) )
139 130 eqeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. <-> <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. ) )
140 132 eqeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. <-> <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. ) )
141 136 eqeq2d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. <-> <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) )
142 139 140 141 3orbi123d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) <-> ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) ) )
143 142 imbi1d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> X = Y ) <-> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) ) )
144 138 143 imbi12d 
 |-  ( ( 2nd ` <. 1 , X >. ) = X -> ( ( ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> X = Y ) ) <-> ( ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) ) ) )
145 127 144 syl 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> X = Y ) ) <-> ( ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , X >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( X - K ) mod N ) >. ) -> X = Y ) ) ) )
146 124 145 mpbird 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> X = Y ) ) )
147 31 146 syld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> X = Y ) ) )
148 147 com23 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) + K ) mod N ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 0 , ( 2nd ` <. 1 , X >. ) >. \/ <. 1 , ( ( Y - K ) mod N ) >. = <. 1 , ( ( ( 2nd ` <. 1 , X >. ) - K ) mod N ) >. ) -> ( { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E -> X = Y ) ) )
149 25 148 syld 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E -> ( { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E -> X = Y ) ) )
150 149 impd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) -> X = Y ) )
151 eqid 
 |-  1 = 1
152 151 olci 
 |-  ( 1 = 0 \/ 1 = 1 )
153 152 2a1i 
 |-  ( Y e. I -> ( X e. I -> ( 1 = 0 \/ 1 = 1 ) ) )
154 153 imdistanri 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( 1 = 0 \/ 1 = 1 ) /\ Y e. I ) )
155 154 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( 1 = 0 \/ 1 = 1 ) /\ Y e. I ) )
156 2 1 3 21 opgpgvtx 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( <. 1 , Y >. e. ( Vtx ` G ) <-> ( ( 1 = 0 \/ 1 = 1 ) /\ Y e. I ) ) )
157 9 156 syl 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , Y >. e. ( Vtx ` G ) <-> ( ( 1 = 0 \/ 1 = 1 ) /\ Y e. I ) ) )
158 157 3adant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( <. 1 , Y >. e. ( Vtx ` G ) <-> ( ( 1 = 0 \/ 1 = 1 ) /\ Y e. I ) ) )
159 155 158 mpbird 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> <. 1 , Y >. e. ( Vtx ` G ) )
160 12 a1i 
 |-  ( X e. I -> 1 e. _V )
161 op1stg 
 |-  ( ( 1 e. _V /\ Y e. I ) -> ( 1st ` <. 1 , Y >. ) = 1 )
162 160 161 sylan 
 |-  ( ( X e. I /\ Y e. I ) -> ( 1st ` <. 1 , Y >. ) = 1 )
163 162 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( 1st ` <. 1 , Y >. ) = 1 )
164 1 3 21 4 gpgedgvtx1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( <. 1 , Y >. e. ( Vtx ` G ) /\ ( 1st ` <. 1 , Y >. ) = 1 ) ) -> ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 0 , ( 2nd ` <. 1 , Y >. ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E ) )
165 10 159 163 164 syl12anc 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 0 , ( 2nd ` <. 1 , Y >. ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E ) )
166 op2ndg 
 |-  ( ( 1 e. _V /\ Y e. I ) -> ( 2nd ` <. 1 , Y >. ) = Y )
167 12 166 mpan 
 |-  ( Y e. I -> ( 2nd ` <. 1 , Y >. ) = Y )
168 oveq1 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> ( ( 2nd ` <. 1 , Y >. ) - K ) = ( Y - K ) )
169 168 oveq1d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) = ( ( Y - K ) mod N ) )
170 169 opeq2d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. = <. 1 , ( ( Y - K ) mod N ) >. )
171 170 preq2d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } = { <. 1 , Y >. , <. 1 , ( ( Y - K ) mod N ) >. } )
172 prcom 
 |-  { <. 1 , Y >. , <. 1 , ( ( Y - K ) mod N ) >. } = { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. }
173 171 172 eqtrdi 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } = { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } )
174 173 eleq1d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E <-> { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E ) )
175 oveq1 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> ( ( 2nd ` <. 1 , Y >. ) + K ) = ( Y + K ) )
176 175 oveq1d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) = ( ( Y + K ) mod N ) )
177 176 opeq2d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. )
178 177 preq2d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } = { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } )
179 178 eleq1d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E <-> { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) )
180 174 179 anbi12d 
 |-  ( ( 2nd ` <. 1 , Y >. ) = Y -> ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E ) <-> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
181 167 180 syl 
 |-  ( Y e. I -> ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E ) <-> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
182 181 biimpcd 
 |-  ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E ) -> ( Y e. I -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
183 182 ancoms 
 |-  ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E ) -> ( Y e. I -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
184 183 3adant2 
 |-  ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 0 , ( 2nd ` <. 1 , Y >. ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E ) -> ( Y e. I -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
185 184 com12 
 |-  ( Y e. I -> ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 0 , ( 2nd ` <. 1 , Y >. ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E ) -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
186 185 adantl 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 0 , ( 2nd ` <. 1 , Y >. ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E ) -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
187 186 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) + K ) mod N ) >. } e. E /\ { <. 1 , Y >. , <. 0 , ( 2nd ` <. 1 , Y >. ) >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( ( 2nd ` <. 1 , Y >. ) - K ) mod N ) >. } e. E ) -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
188 165 187 mpd 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) )
189 opeq2 
 |-  ( X = Y -> <. 1 , X >. = <. 1 , Y >. )
190 189 preq2d 
 |-  ( X = Y -> { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } = { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } )
191 190 eleq1d 
 |-  ( X = Y -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E <-> { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E ) )
192 189 preq1d 
 |-  ( X = Y -> { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } = { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } )
193 192 eleq1d 
 |-  ( X = Y -> ( { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E <-> { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) )
194 191 193 anbi12d 
 |-  ( X = Y -> ( ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) <-> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , Y >. } e. E /\ { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
195 188 194 syl5ibrcom 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( X = Y -> ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) ) )
196 150 195 impbid 
 |-  ( ( N e. ( ZZ>= ` 5 ) /\ ( X e. I /\ Y e. I ) /\ ( K e. J /\ ( ( 4 x. K ) mod N ) =/= 0 ) ) -> ( ( { <. 1 , ( ( Y - K ) mod N ) >. , <. 1 , X >. } e. E /\ { <. 1 , X >. , <. 1 , ( ( Y + K ) mod N ) >. } e. E ) <-> X = Y ) )