Metamath Proof Explorer

Theorem gpg5nbgrvtx13starlem1

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