Metamath Proof Explorer

Theorem gpg5nbgrvtx03starlem3

Description: Lemma 3 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 gpg5nbgrvtx03starlem3 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } 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 
 |-  <. 1 , X >. e. _V
6 opex 
 |-  <. 0 , ( ( X - 1 ) mod N ) >. e. _V
7 5 6 pm3.2i 
 |-  ( <. 1 , X >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. 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 
 |-  ( ( <. 1 , X >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) )
12 ax-1ne0 
 |-  1 =/= 0
13 12 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> 1 =/= 0 )
14 13 orcd 
 |-  ( ( ( 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 orci 
 |-  ( 1 =/= 0 \/ X =/= ( ( x + 1 ) mod N ) )
24 23 a1i 
 |-  ( ( ( 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 orcd 
 |-  ( ( ( 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 ) >. ) \/ ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. /\ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) )
30 prneimg 
 |-  ( ( ( <. 1 , X >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) ) -> ( ( ( <. 1 , X >. =/= <. 0 , x >. /\ <. 1 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) \/ ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. /\ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) -> { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 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 ) ) -> { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 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 m1modne 
 |-  ( ( 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 6 5 pm3.2i 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V )
67 opex 
 |-  <. 1 , x >. e. _V
68 8 67 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V )
69 66 68 pm3.2i 
 |-  ( ( <. 0 , ( ( X - 1 ) mod N ) >. e. _V /\ <. 1 , X >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) )
70 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 >. ) ) ) )
71 69 70 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 >. ) ) ) )
72 65 71 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 >. } )
73 prcom 
 |-  { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , ( ( X - 1 ) mod N ) >. , <. 1 , X >. }
74 73 neeq1i 
 |-  ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , ( ( X - 1 ) mod N ) >. , <. 1 , X >. } =/= { <. 0 , x >. , <. 1 , x >. } )
75 72 74 sylibr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } )
76 opex 
 |-  <. 1 , ( ( x + K ) mod N ) >. e. _V
77 67 76 pm3.2i 
 |-  ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V )
78 7 77 pm3.2i 
 |-  ( ( <. 1 , X >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) )
79 0ne1 
 |-  0 =/= 1
80 79 orci 
 |-  ( 0 =/= 1 \/ ( ( X - 1 ) mod N ) =/= x )
81 50 51 opthne 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ ( ( X - 1 ) mod N ) =/= x ) )
82 80 81 mpbir 
 |-  <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >.
83 79 orci 
 |-  ( 0 =/= 1 \/ ( ( X - 1 ) mod N ) =/= ( ( x + K ) mod N ) )
84 50 51 opthne 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 0 =/= 1 \/ ( ( X - 1 ) mod N ) =/= ( ( x + K ) mod N ) ) )
85 83 84 mpbir 
 |-  <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >.
86 82 85 pm3.2i 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. )
87 86 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 ) >. ) )
88 87 olcd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 1 , X >. =/= <. 1 , x >. /\ <. 1 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. ) \/ ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) )
89 prneimg 
 |-  ( ( ( <. 1 , X >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) ) -> ( ( ( <. 1 , X >. =/= <. 1 , x >. /\ <. 1 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. ) \/ ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) -> { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
90 78 88 89 mpsyl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
91 31 75 90 3jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
92 91 ralrimiva 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> A. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
93 ralnex 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> -. E. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
94 3ioran 
 |-  ( -. ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
95 df-ne 
 |-  ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
96 df-ne 
 |-  ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } )
97 df-ne 
 |-  ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
98 95 96 97 3anbi123i 
 |-  ( ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
99 94 98 bitr4i 
 |-  ( -. ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
100 99 ralbii 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
101 93 100 bitr3i 
 |-  ( -. E. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
102 92 101 sylibr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> -. E. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
103 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
104 103 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
105 104 3adant3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
106 102 105 mtbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E )
107 df-nel 
 |-  ( { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } e/ E <-> -. { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E )
108 106 107 sylibr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. W ) -> { <. 1 , X >. , <. 0 , ( ( X - 1 ) mod N ) >. } e/ E )