Metamath Proof Explorer

Theorem gpg5nbgrvtx03starlem1

Description: Lemma 1 for gpg5nbgrvtx03star . (Contributed by AV, 5-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 gpg5nbgrvtx03starlem1.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpg5nbgrvtx03starlem1.g 
 |-  G = ( N gPetersenGr K )
3 gpg5nbgrvtx03starlem1.v 
 |-  V = ( Vtx ` G )
4 gpg5nbgrvtx03starlem1.e 
 |-  E = ( Edg ` G )
5 opex 
 |-  <. 0 , ( ( X + 1 ) mod N ) >. e. _V
6 opex 
 |-  <. 1 , X >. e. _V
7 5 6 pm3.2i 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V )
8 opex 
 |-  <. 0 , x >. e. _V
9 opex 
 |-  <. 0 , ( ( x + 1 ) mod N ) >. e. _V
10 8 9 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V )
11 7 10 pm3.2i 
 |-  ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) )
12 ax-1ne0 
 |-  1 =/= 0
13 12 orci 
 |-  ( 1 =/= 0 \/ X =/= x )
14 13 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( 1 =/= 0 \/ X =/= x ) )
15 1ex 
 |-  1 e. _V
16 15 a1i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> 1 e. _V )
17 simp3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> X e. W )
18 16 17 jca 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> ( 1 e. _V /\ X e. W ) )
19 18 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( 1 e. _V /\ X e. W ) )
20 opthneg 
 |-  ( ( 1 e. _V /\ X e. W ) -> ( <. 1 , X >. =/= <. 0 , x >. <-> ( 1 =/= 0 \/ X =/= x ) ) )
21 19 20 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , X >. =/= <. 0 , x >. <-> ( 1 =/= 0 \/ X =/= x ) ) )
22 14 21 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> <. 1 , X >. =/= <. 0 , x >. )
23 12 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> 1 =/= 0 )
24 23 orcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( 1 =/= 0 \/ X =/= ( ( x + 1 ) mod N ) ) )
25 opthneg 
 |-  ( ( 1 e. _V /\ X e. W ) -> ( <. 1 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( 1 =/= 0 \/ X =/= ( ( x + 1 ) mod N ) ) ) )
26 19 25 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( 1 =/= 0 \/ X =/= ( ( x + 1 ) mod N ) ) ) )
27 24 26 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> <. 1 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. )
28 22 27 jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , X >. =/= <. 0 , x >. /\ <. 1 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) )
29 28 olcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) \/ ( <. 1 , X >. =/= <. 0 , x >. /\ <. 1 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) )
30 prneimg 
 |-  ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) ) -> ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) \/ ( <. 1 , X >. =/= <. 0 , x >. /\ <. 1 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
31 11 29 30 mpsyl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
32 eleq1 
 |-  ( X = x -> ( X e. ( 0 ..^ N ) <-> x e. ( 0 ..^ N ) ) )
33 32 adantr 
 |-  ( ( X = x /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) ) -> ( X e. ( 0 ..^ N ) <-> x e. ( 0 ..^ N ) ) )
34 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
35 34 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> N e. ( ZZ>= ` 2 ) )
36 p1modne 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ X e. ( 0 ..^ N ) ) -> ( ( X + 1 ) mod N ) =/= X )
37 35 36 sylan 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ X e. ( 0 ..^ N ) ) -> ( ( X + 1 ) mod N ) =/= X )
38 37 ex 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> ( X e. ( 0 ..^ N ) -> ( ( X + 1 ) mod N ) =/= X ) )
39 38 adantl 
 |-  ( ( X = x /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) ) -> ( X e. ( 0 ..^ N ) -> ( ( X + 1 ) mod N ) =/= X ) )
40 33 39 sylbird 
 |-  ( ( X = x /\ ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) ) -> ( x e. ( 0 ..^ N ) -> ( ( X + 1 ) mod N ) =/= X ) )
41 40 impr 
 |-  ( ( X = x /\ ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X + 1 ) mod N ) =/= X )
42 neeq2 
 |-  ( X = x -> ( ( ( X + 1 ) mod N ) =/= X <-> ( ( X + 1 ) mod N ) =/= x ) )
43 42 adantr 
 |-  ( ( X = x /\ ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X + 1 ) mod N ) =/= X <-> ( ( X + 1 ) mod N ) =/= x ) )
44 41 43 mpbid 
 |-  ( ( X = x /\ ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X + 1 ) mod N ) =/= x )
45 44 orcd 
 |-  ( ( X = x /\ ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ X =/= x ) )
46 45 ex 
 |-  ( X = x -> ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ X =/= x ) ) )
47 olc 
 |-  ( X =/= x -> ( ( ( X + 1 ) mod N ) =/= x \/ X =/= x ) )
48 47 a1d 
 |-  ( X =/= x -> ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ X =/= x ) ) )
49 46 48 pm2.61ine 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ X =/= x ) )
50 c0ex 
 |-  0 e. _V
51 ovex 
 |-  ( ( X + 1 ) mod N ) e. _V
52 50 51 opthne 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. <-> ( 0 =/= 0 \/ ( ( X + 1 ) mod N ) =/= x ) )
53 neirr 
 |-  -. 0 =/= 0
54 53 biorfi 
 |-  ( ( ( X + 1 ) mod N ) =/= x <-> ( 0 =/= 0 \/ ( ( X + 1 ) mod N ) =/= x ) )
55 52 54 bitr4i 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. <-> ( ( X + 1 ) mod N ) =/= x )
56 55 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. <-> ( ( X + 1 ) mod N ) =/= x ) )
57 opthneg 
 |-  ( ( 1 e. _V /\ X e. W ) -> ( <. 1 , X >. =/= <. 1 , x >. <-> ( 1 =/= 1 \/ X =/= x ) ) )
58 19 57 syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , X >. =/= <. 1 , x >. <-> ( 1 =/= 1 \/ X =/= x ) ) )
59 neirr 
 |-  -. 1 =/= 1
60 59 biorfi 
 |-  ( X =/= x <-> ( 1 =/= 1 \/ X =/= x ) )
61 58 60 bitr4di 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , X >. =/= <. 1 , x >. <-> X =/= x ) )
62 56 61 orbi12d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , X >. =/= <. 1 , x >. ) <-> ( ( ( X + 1 ) mod N ) =/= x \/ X =/= x ) ) )
63 49 62 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , X >. =/= <. 1 , x >. ) )
64 22 olcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , X >. =/= <. 0 , x >. ) )
65 63 64 jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , X >. =/= <. 1 , x >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , X >. =/= <. 0 , x >. ) ) )
66 opex 
 |-  <. 1 , x >. e. _V
67 8 66 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V )
68 7 67 pm3.2i 
 |-  ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) )
69 prneimg2 
 |-  ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , X >. =/= <. 1 , x >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , X >. =/= <. 0 , x >. ) ) ) )
70 68 69 mp1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , X >. =/= <. 1 , x >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , X >. =/= <. 0 , x >. ) ) ) )
71 65 70 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } )
72 opex 
 |-  <. 1 , ( ( x + K ) mod N ) >. e. _V
73 66 72 pm3.2i 
 |-  ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V )
74 7 73 pm3.2i 
 |-  ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) )
75 0ne1 
 |-  0 =/= 1
76 75 orci 
 |-  ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= x )
77 50 51 opthne 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= x ) )
78 76 77 mpbir 
 |-  <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >.
79 75 orci 
 |-  ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= ( ( x + K ) mod N ) )
80 50 51 opthne 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= ( ( x + K ) mod N ) ) )
81 79 80 mpbir 
 |-  <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >.
82 78 81 pm3.2i 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. )
83 82 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) )
84 83 orcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) \/ ( <. 1 , X >. =/= <. 1 , x >. /\ <. 1 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) )
85 prneimg 
 |-  ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) ) -> ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) \/ ( <. 1 , X >. =/= <. 1 , x >. /\ <. 1 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
86 74 84 85 mpsyl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
87 31 71 86 3jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
88 87 ralrimiva 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> A. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
89 ralnex 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> -. E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
90 3ioran 
 |-  ( -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
91 df-ne 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
92 df-ne 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } )
93 df-ne 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
94 91 92 93 3anbi123i 
 |-  ( ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
95 90 94 bitr4i 
 |-  ( -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
96 95 ralbii 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
97 89 96 bitr3i 
 |-  ( -. E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
98 88 97 sylibr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> -. E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
99 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
100 99 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
101 100 3adant3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
102 98 101 mtbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } e. E )
103 df-nel 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } e/ E <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } e. E )
104 102 103 sylibr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 1 , X >. } e/ E )