Metamath Proof Explorer

Theorem gpg5nbgrvtx03starlem2

Description: Lemma 2 for gpg5nbgrvtx03star . (Contributed by AV, 6-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 gpg5nbgrvtx03starlem2 
|- ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 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 m1modnep2mod 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ X e. ZZ ) -> ( ( X - 1 ) mod N ) =/= ( ( X + 2 ) mod N ) )
6 5 3adant2 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X - 1 ) mod N ) =/= ( ( X + 2 ) mod N ) )
7 zcn 
 |-  ( X e. ZZ -> X e. CC )
8 7 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> X e. CC )
9 add1p1 
 |-  ( X e. CC -> ( ( X + 1 ) + 1 ) = ( X + 2 ) )
10 8 9 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X + 1 ) + 1 ) = ( X + 2 ) )
11 10 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( ( X + 1 ) + 1 ) mod N ) = ( ( X + 2 ) mod N ) )
12 6 11 neeqtrrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X - 1 ) mod N ) =/= ( ( ( X + 1 ) + 1 ) mod N ) )
13 zre 
 |-  ( X e. ZZ -> X e. RR )
14 13 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> X e. RR )
15 1red 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> 1 e. RR )
16 14 15 readdcld 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( X + 1 ) e. RR )
17 eluz4nn 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. NN )
18 17 nnrpd 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. RR+ )
19 18 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> N e. RR+ )
20 modaddmod 
 |-  ( ( ( X + 1 ) e. RR /\ 1 e. RR /\ N e. RR+ ) -> ( ( ( ( X + 1 ) mod N ) + 1 ) mod N ) = ( ( ( X + 1 ) + 1 ) mod N ) )
21 16 15 19 20 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( ( ( X + 1 ) mod N ) + 1 ) mod N ) = ( ( ( X + 1 ) + 1 ) mod N ) )
22 12 21 neeqtrrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X - 1 ) mod N ) =/= ( ( ( ( X + 1 ) mod N ) + 1 ) mod N ) )
23 22 ad2antrl 
 |-  ( ( ( ( X + 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X - 1 ) mod N ) =/= ( ( ( ( X + 1 ) mod N ) + 1 ) mod N ) )
24 oveq1 
 |-  ( ( ( X + 1 ) mod N ) = x -> ( ( ( X + 1 ) mod N ) + 1 ) = ( x + 1 ) )
25 24 oveq1d 
 |-  ( ( ( X + 1 ) mod N ) = x -> ( ( ( ( X + 1 ) mod N ) + 1 ) mod N ) = ( ( x + 1 ) mod N ) )
26 25 adantr 
 |-  ( ( ( ( X + 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( ( X + 1 ) mod N ) + 1 ) mod N ) = ( ( x + 1 ) mod N ) )
27 23 26 neeqtrd 
 |-  ( ( ( ( X + 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) )
28 27 olcd 
 |-  ( ( ( ( X + 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
29 28 ex 
 |-  ( ( ( X + 1 ) mod N ) = x -> ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) ) )
30 orc 
 |-  ( ( ( X + 1 ) mod N ) =/= x -> ( ( ( X + 1 ) mod N ) =/= x \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
31 30 a1d 
 |-  ( ( ( X + 1 ) mod N ) =/= x -> ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) ) )
32 29 31 pm2.61ine 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= x \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
33 c0ex 
 |-  0 e. _V
34 ovex 
 |-  ( ( X + 1 ) mod N ) e. _V
35 33 34 opthne 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. <-> ( 0 =/= 0 \/ ( ( X + 1 ) mod N ) =/= x ) )
36 neirr 
 |-  -. 0 =/= 0
37 36 biorfi 
 |-  ( ( ( X + 1 ) mod N ) =/= x <-> ( 0 =/= 0 \/ ( ( X + 1 ) mod N ) =/= x ) )
38 35 37 bitr4i 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. <-> ( ( X + 1 ) mod N ) =/= x )
39 38 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. <-> ( ( X + 1 ) mod N ) =/= x ) )
40 ovex 
 |-  ( ( X - 1 ) mod N ) e. _V
41 33 40 opthne 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( 0 =/= 0 \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
42 36 biorfi 
 |-  ( ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) <-> ( 0 =/= 0 \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
43 41 42 bitr4i 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) )
44 43 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
45 39 44 orbi12d 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) <-> ( ( ( X + 1 ) mod N ) =/= x \/ ( ( X - 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) ) )
46 32 45 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) )
47 eluz4eluz2 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. ( ZZ>= ` 2 ) )
48 47 anim1i 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ X e. ZZ ) -> ( N e. ( ZZ>= ` 2 ) /\ X e. ZZ ) )
49 48 3adant2 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( N e. ( ZZ>= ` 2 ) /\ X e. ZZ ) )
50 zp1modne 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ X e. ZZ ) -> ( ( X + 1 ) mod N ) =/= ( X mod N ) )
51 49 50 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X + 1 ) mod N ) =/= ( X mod N ) )
52 npcan1 
 |-  ( X e. CC -> ( ( X - 1 ) + 1 ) = X )
53 8 52 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X - 1 ) + 1 ) = X )
54 53 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( ( X - 1 ) + 1 ) mod N ) = ( X mod N ) )
55 51 54 neeqtrrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X + 1 ) mod N ) =/= ( ( ( X - 1 ) + 1 ) mod N ) )
56 14 15 resubcld 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( X - 1 ) e. RR )
57 modaddmod 
 |-  ( ( ( X - 1 ) e. RR /\ 1 e. RR /\ N e. RR+ ) -> ( ( ( ( X - 1 ) mod N ) + 1 ) mod N ) = ( ( ( X - 1 ) + 1 ) mod N ) )
58 56 15 19 57 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( ( ( X - 1 ) mod N ) + 1 ) mod N ) = ( ( ( X - 1 ) + 1 ) mod N ) )
59 55 58 neeqtrrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( ( X + 1 ) mod N ) =/= ( ( ( ( X - 1 ) mod N ) + 1 ) mod N ) )
60 59 ad2antrl 
 |-  ( ( ( ( X - 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X + 1 ) mod N ) =/= ( ( ( ( X - 1 ) mod N ) + 1 ) mod N ) )
61 oveq1 
 |-  ( ( ( X - 1 ) mod N ) = x -> ( ( ( X - 1 ) mod N ) + 1 ) = ( x + 1 ) )
62 61 oveq1d 
 |-  ( ( ( X - 1 ) mod N ) = x -> ( ( ( ( X - 1 ) mod N ) + 1 ) mod N ) = ( ( x + 1 ) mod N ) )
63 62 adantr 
 |-  ( ( ( ( X - 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( ( X - 1 ) mod N ) + 1 ) mod N ) = ( ( x + 1 ) mod N ) )
64 60 63 neeqtrd 
 |-  ( ( ( ( X - 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) )
65 64 orcd 
 |-  ( ( ( ( X - 1 ) mod N ) = x /\ ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) \/ ( ( X - 1 ) mod N ) =/= x ) )
66 65 ex 
 |-  ( ( ( X - 1 ) mod N ) = x -> ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) \/ ( ( X - 1 ) mod N ) =/= x ) ) )
67 olc 
 |-  ( ( ( X - 1 ) mod N ) =/= x -> ( ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) \/ ( ( X - 1 ) mod N ) =/= x ) )
68 67 a1d 
 |-  ( ( ( X - 1 ) mod N ) =/= x -> ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) \/ ( ( X - 1 ) mod N ) =/= x ) ) )
69 66 68 pm2.61ine 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) \/ ( ( X - 1 ) mod N ) =/= x ) )
70 33 34 opthne 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( 0 =/= 0 \/ ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
71 36 biorfi 
 |-  ( ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) <-> ( 0 =/= 0 \/ ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
72 70 71 bitr4i 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) )
73 72 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) ) )
74 33 40 opthne 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. <-> ( 0 =/= 0 \/ ( ( X - 1 ) mod N ) =/= x ) )
75 36 biorfi 
 |-  ( ( ( X - 1 ) mod N ) =/= x <-> ( 0 =/= 0 \/ ( ( X - 1 ) mod N ) =/= x ) )
76 74 75 bitr4i 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. <-> ( ( X - 1 ) mod N ) =/= x )
77 76 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. <-> ( ( X - 1 ) mod N ) =/= x ) )
78 73 77 orbi12d 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) <-> ( ( ( X + 1 ) mod N ) =/= ( ( x + 1 ) mod N ) \/ ( ( X - 1 ) mod N ) =/= x ) ) )
79 69 78 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) )
80 opex 
 |-  <. 0 , ( ( X + 1 ) mod N ) >. e. _V
81 opex 
 |-  <. 0 , ( ( X - 1 ) mod N ) >. e. _V
82 80 81 pm3.2i 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V )
83 opex 
 |-  <. 0 , x >. e. _V
84 opex 
 |-  <. 0 , ( ( x + 1 ) mod N ) >. e. _V
85 83 84 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V )
86 82 85 pm3.2i 
 |-  ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) )
87 prneimg2 
 |-  ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) ) ) )
88 86 87 mp1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) ) ) )
89 46 79 88 mpbir2and 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
90 0ne1 
 |-  0 =/= 1
91 90 orci 
 |-  ( 0 =/= 1 \/ ( ( X - 1 ) mod N ) =/= x )
92 33 40 opthne 
 |-  ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ ( ( X - 1 ) mod N ) =/= x ) )
93 91 92 mpbir 
 |-  <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >.
94 93 olci 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. )
95 90 orci 
 |-  ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= x )
96 33 34 opthne 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= x ) )
97 95 96 mpbir 
 |-  <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >.
98 97 orci 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. )
99 94 98 pm3.2i 
 |-  ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) )
100 99 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) ) )
101 opex 
 |-  <. 1 , x >. e. _V
102 83 101 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V )
103 82 102 pm3.2i 
 |-  ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) )
104 prneimg2 
 |-  ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) ) ) )
105 103 104 mp1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 0 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. \/ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 0 , x >. ) ) ) )
106 100 105 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } )
107 opex 
 |-  <. 1 , ( ( x + K ) mod N ) >. e. _V
108 101 107 pm3.2i 
 |-  ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V )
109 82 108 pm3.2i 
 |-  ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) )
110 90 orci 
 |-  ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= ( ( x + K ) mod N ) )
111 33 34 opthne 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 0 =/= 1 \/ ( ( X + 1 ) mod N ) =/= ( ( x + K ) mod N ) ) )
112 110 111 mpbir 
 |-  <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >.
113 97 112 pm3.2i 
 |-  ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. )
114 113 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) )
115 114 orcd 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X + 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) \/ ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) )
116 prneimg 
 |-  ( ( ( <. 0 , ( ( X + 1 ) mod N ) >. e. _V /\ <. 0 , ( ( X - 1 ) mod N ) >. 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 ) >. ) \/ ( <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , x >. /\ <. 0 , ( ( X - 1 ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
117 109 115 116 mpsyl 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
118 89 106 117 3jca 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
119 118 ralrimiva 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> A. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
120 ralnex 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> -. E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
121 3ioran 
 |-  ( -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
122 df-ne 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
123 df-ne 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } )
124 df-ne 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
125 122 123 124 3anbi123i 
 |-  ( ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
126 121 125 bitr4i 
 |-  ( -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
127 126 ralbii 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
128 120 127 bitr3i 
 |-  ( -. E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
129 119 128 sylibr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> -. E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
130 eluz4eluz3 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. ( ZZ>= ` 3 ) )
131 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
132 131 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
133 130 132 sylan 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
134 133 3adant3 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
135 129 134 mtbird 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E )
136 df-nel 
 |-  ( { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } e/ E <-> -. { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } e. E )
137 135 136 sylibr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ K e. J /\ X e. ZZ ) -> { <. 0 , ( ( X + 1 ) mod N ) >. , <. 0 , ( ( X - 1 ) mod N ) >. } e/ E )