Metamath Proof Explorer

Theorem gpg5nbgrvtx13starlem3

Description: Lemma 3 for gpg5nbgr3star . (Contributed by AV, 8-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 gpg5nbgrvtx13starlem3 
|- ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> { <. 0 , X >. , <. 1 , ( ( X - K ) 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 
 |-  <. 0 , X >. e. _V
6 opex 
 |-  <. 1 , ( ( X - K ) mod N ) >. e. _V
7 5 6 pm3.2i 
 |-  ( <. 0 , X >. e. _V /\ <. 1 , ( ( X - K ) 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 
 |-  ( ( <. 0 , X >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) )
12 ax-1ne0 
 |-  1 =/= 0
13 12 orci 
 |-  ( 1 =/= 0 \/ ( ( X - K ) mod N ) =/= x )
14 1ex 
 |-  1 e. _V
15 ovex 
 |-  ( ( X - K ) mod N ) e. _V
16 14 15 opthne 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. <-> ( 1 =/= 0 \/ ( ( X - K ) mod N ) =/= x ) )
17 13 16 mpbir 
 |-  <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >.
18 12 orci 
 |-  ( 1 =/= 0 \/ ( ( X - K ) mod N ) =/= ( ( x + 1 ) mod N ) )
19 14 15 opthne 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( 1 =/= 0 \/ ( ( X - K ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
20 18 19 mpbir 
 |-  <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >.
21 17 20 pm3.2i 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. )
22 21 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) )
23 22 olcd 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , X >. =/= <. 0 , x >. /\ <. 0 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) \/ ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) )
24 prneimg 
 |-  ( ( ( <. 0 , X >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) ) -> ( ( ( <. 0 , X >. =/= <. 0 , x >. /\ <. 0 , X >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) \/ ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) -> { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
25 11 23 24 mpsyl 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
26 eleq1 
 |-  ( X = x -> ( X e. ( 0 ..^ N ) <-> x e. ( 0 ..^ N ) ) )
27 26 adantr 
 |-  ( ( X = x /\ ( ( N = 5 /\ K e. J ) /\ X e. W ) ) -> ( X e. ( 0 ..^ N ) <-> x e. ( 0 ..^ N ) ) )
28 simpll 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> N = 5 )
29 28 oveq2d 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> ( 0 ..^ N ) = ( 0 ..^ 5 ) )
30 29 eleq2d 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> ( X e. ( 0 ..^ N ) <-> X e. ( 0 ..^ 5 ) ) )
31 30 biimpa 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ X e. ( 0 ..^ N ) ) -> X e. ( 0 ..^ 5 ) )
32 5nn 
 |-  5 e. NN
33 eleq1 
 |-  ( N = 5 -> ( N e. NN <-> 5 e. NN ) )
34 32 33 mpbiri 
 |-  ( N = 5 -> N e. NN )
35 1 ceilhalfelfzo1 
 |-  ( N e. NN -> ( K e. J -> K e. ( 1 ..^ N ) ) )
36 34 35 syl 
 |-  ( N = 5 -> ( K e. J -> K e. ( 1 ..^ N ) ) )
37 oveq2 
 |-  ( N = 5 -> ( 1 ..^ N ) = ( 1 ..^ 5 ) )
38 37 eleq2d 
 |-  ( N = 5 -> ( K e. ( 1 ..^ N ) <-> K e. ( 1 ..^ 5 ) ) )
39 36 38 sylibd 
 |-  ( N = 5 -> ( K e. J -> K e. ( 1 ..^ 5 ) ) )
40 39 imp 
 |-  ( ( N = 5 /\ K e. J ) -> K e. ( 1 ..^ 5 ) )
41 40 ad2antrr 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ X e. ( 0 ..^ N ) ) -> K e. ( 1 ..^ 5 ) )
42 minusmod5ne 
 |-  ( ( X e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( ( X - K ) mod 5 ) =/= X )
43 31 41 42 syl2anc 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ X e. ( 0 ..^ N ) ) -> ( ( X - K ) mod 5 ) =/= X )
44 oveq2 
 |-  ( N = 5 -> ( ( X - K ) mod N ) = ( ( X - K ) mod 5 ) )
45 44 neeq1d 
 |-  ( N = 5 -> ( ( ( X - K ) mod N ) =/= X <-> ( ( X - K ) mod 5 ) =/= X ) )
46 45 adantr 
 |-  ( ( N = 5 /\ K e. J ) -> ( ( ( X - K ) mod N ) =/= X <-> ( ( X - K ) mod 5 ) =/= X ) )
47 46 ad2antrr 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ X e. ( 0 ..^ N ) ) -> ( ( ( X - K ) mod N ) =/= X <-> ( ( X - K ) mod 5 ) =/= X ) )
48 43 47 mpbird 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ X e. ( 0 ..^ N ) ) -> ( ( X - K ) mod N ) =/= X )
49 48 ex 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> ( X e. ( 0 ..^ N ) -> ( ( X - K ) mod N ) =/= X ) )
50 49 adantl 
 |-  ( ( X = x /\ ( ( N = 5 /\ K e. J ) /\ X e. W ) ) -> ( X e. ( 0 ..^ N ) -> ( ( X - K ) mod N ) =/= X ) )
51 27 50 sylbird 
 |-  ( ( X = x /\ ( ( N = 5 /\ K e. J ) /\ X e. W ) ) -> ( x e. ( 0 ..^ N ) -> ( ( X - K ) mod N ) =/= X ) )
52 51 impr 
 |-  ( ( X = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X - K ) mod N ) =/= X )
53 neeq2 
 |-  ( X = x -> ( ( ( X - K ) mod N ) =/= X <-> ( ( X - K ) mod N ) =/= x ) )
54 53 adantr 
 |-  ( ( X = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X - K ) mod N ) =/= X <-> ( ( X - K ) mod N ) =/= x ) )
55 52 54 mpbid 
 |-  ( ( X = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X - K ) mod N ) =/= x )
56 55 orcd 
 |-  ( ( X = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X - K ) mod N ) =/= x \/ X =/= x ) )
57 56 ex 
 |-  ( X = x -> ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X - K ) mod N ) =/= x \/ X =/= x ) ) )
58 olc 
 |-  ( X =/= x -> ( ( ( X - K ) mod N ) =/= x \/ X =/= x ) )
59 58 a1d 
 |-  ( X =/= x -> ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X - K ) mod N ) =/= x \/ X =/= x ) ) )
60 57 59 pm2.61ine 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X - K ) mod N ) =/= x \/ X =/= x ) )
61 14 15 opthne 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. <-> ( 1 =/= 1 \/ ( ( X - K ) mod N ) =/= x ) )
62 neirr 
 |-  -. 1 =/= 1
63 62 biorfi 
 |-  ( ( ( X - K ) mod N ) =/= x <-> ( 1 =/= 1 \/ ( ( X - K ) mod N ) =/= x ) )
64 61 63 bitr4i 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. <-> ( ( X - K ) mod N ) =/= x )
65 64 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. <-> ( ( X - K ) mod N ) =/= x ) )
66 c0ex 
 |-  0 e. _V
67 66 a1i 
 |-  ( ( N = 5 /\ K e. J ) -> 0 e. _V )
68 67 anim1i 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> ( 0 e. _V /\ X e. W ) )
69 68 adantr 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( 0 e. _V /\ X e. W ) )
70 opthneg 
 |-  ( ( 0 e. _V /\ X e. W ) -> ( <. 0 , X >. =/= <. 0 , x >. <-> ( 0 =/= 0 \/ X =/= x ) ) )
71 69 70 syl 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , X >. =/= <. 0 , x >. <-> ( 0 =/= 0 \/ X =/= x ) ) )
72 neirr 
 |-  -. 0 =/= 0
73 72 biorfi 
 |-  ( X =/= x <-> ( 0 =/= 0 \/ X =/= x ) )
74 71 73 bitr4di 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , X >. =/= <. 0 , x >. <-> X =/= x ) )
75 65 74 orbi12d 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. \/ <. 0 , X >. =/= <. 0 , x >. ) <-> ( ( ( X - K ) mod N ) =/= x \/ X =/= x ) ) )
76 60 75 mpbird 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. \/ <. 0 , X >. =/= <. 0 , x >. ) )
77 76 orcomd 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , X >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) )
78 0ne1 
 |-  0 =/= 1
79 78 orci 
 |-  ( 0 =/= 1 \/ X =/= x )
80 opthneg 
 |-  ( ( 0 e. _V /\ X e. W ) -> ( <. 0 , X >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ X =/= x ) ) )
81 69 80 syl 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , X >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ X =/= x ) ) )
82 79 81 mpbiri 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> <. 0 , X >. =/= <. 1 , x >. )
83 82 orcd 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , X >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. ) )
84 77 83 jca 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , X >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 0 , X >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. ) ) )
85 opex 
 |-  <. 1 , x >. e. _V
86 8 85 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V )
87 7 86 pm3.2i 
 |-  ( ( <. 0 , X >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) )
88 prneimg2 
 |-  ( ( ( <. 0 , X >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) ) -> ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 0 , X >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 0 , X >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. ) ) ) )
89 87 88 mp1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 0 , X >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 0 , X >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. ) ) ) )
90 84 89 mpbird 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } )
91 opex 
 |-  <. 1 , ( ( x + K ) mod N ) >. e. _V
92 85 91 pm3.2i 
 |-  ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V )
93 7 92 pm3.2i 
 |-  ( ( <. 0 , X >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) )
94 78 orci 
 |-  ( 0 =/= 1 \/ X =/= ( ( x + K ) mod N ) )
95 opthneg 
 |-  ( ( 0 e. _V /\ X e. W ) -> ( <. 0 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 0 =/= 1 \/ X =/= ( ( x + K ) mod N ) ) ) )
96 69 95 syl 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 0 =/= 1 \/ X =/= ( ( x + K ) mod N ) ) ) )
97 94 96 mpbiri 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> <. 0 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. )
98 82 97 jca 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , X >. =/= <. 1 , x >. /\ <. 0 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. ) )
99 98 orcd 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , X >. =/= <. 1 , x >. /\ <. 0 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. ) \/ ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) )
100 prneimg 
 |-  ( ( ( <. 0 , X >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) ) -> ( ( ( <. 0 , X >. =/= <. 1 , x >. /\ <. 0 , X >. =/= <. 1 , ( ( x + K ) mod N ) >. ) \/ ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) -> { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
101 93 99 100 mpsyl 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
102 25 90 101 3jca 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. W ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
103 102 ralrimiva 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> A. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
104 ralnex 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> -. E. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
105 3ioran 
 |-  ( -. ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
106 df-ne 
 |-  ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
107 df-ne 
 |-  ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } )
108 df-ne 
 |-  ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
109 106 107 108 3anbi123i 
 |-  ( ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
110 105 109 bitr4i 
 |-  ( -. ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
111 110 ralbii 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
112 104 111 bitr3i 
 |-  ( -. E. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
113 103 112 sylibr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> -. E. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
114 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
115 eleq1 
 |-  ( N = 5 -> ( N e. ( ZZ>= ` 3 ) <-> 5 e. ( ZZ>= ` 3 ) ) )
116 114 115 mpbiri 
 |-  ( N = 5 -> N e. ( ZZ>= ` 3 ) )
117 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
118 117 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
119 116 118 sylan 
 |-  ( ( N = 5 /\ K e. J ) -> ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
120 119 adantr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
121 113 120 mtbird 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } e. E )
122 df-nel 
 |-  ( { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } e/ E <-> -. { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } e. E )
123 121 122 sylibr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. W ) -> { <. 0 , X >. , <. 1 , ( ( X - K ) mod N ) >. } e/ E )