Metamath Proof Explorer

Theorem gpg5nbgrvtx13starlem2

Description: Lemma 2 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 gpg5nbgrvtx13starlem2 
|- ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> { <. 1 , ( ( X + K ) mod N ) >. , <. 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 
 |-  <. 1 , ( ( X + K ) mod N ) >. e. _V
6 opex 
 |-  <. 1 , ( ( X - K ) mod N ) >. e. _V
7 5 6 pm3.2i 
 |-  ( <. 1 , ( ( X + K ) mod N ) >. 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 
 |-  ( ( <. 1 , ( ( X + K ) mod N ) >. 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. ZZ ) /\ 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. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 0 , x >. /\ <. 1 , ( ( X + K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) \/ ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) )
24 prneimg 
 |-  ( ( ( <. 1 , ( ( X + K ) mod N ) >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. 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 ) >. ) \/ ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. /\ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , ( ( x + 1 ) mod N ) >. ) ) -> { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
25 11 23 24 mpsyl 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
26 17 orci 
 |-  ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. )
27 26 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) )
28 12 orci 
 |-  ( 1 =/= 0 \/ ( ( X - K ) mod N ) =/= x )
29 ovex 
 |-  ( ( X - K ) mod N ) e. _V
30 14 29 opthne 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. <-> ( 1 =/= 0 \/ ( ( X - K ) mod N ) =/= x ) )
31 28 30 mpbir 
 |-  <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >.
32 31 olci 
 |-  ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. )
33 32 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. ) )
34 opex 
 |-  <. 1 , x >. e. _V
35 8 34 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V )
36 7 35 pm3.2i 
 |-  ( ( <. 1 , ( ( X + K ) mod N ) >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) )
37 prneimg2 
 |-  ( ( ( <. 1 , ( ( X + K ) mod N ) >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. ) ) ) )
38 36 37 mp1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 0 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) /\ ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 0 , x >. ) ) ) )
39 27 33 38 mpbir2and 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } )
40 fvoveq1 
 |-  ( N = 5 -> ( |^ ` ( N / 2 ) ) = ( |^ ` ( 5 / 2 ) ) )
41 ceil5half3 
 |-  ( |^ ` ( 5 / 2 ) ) = 3
42 40 41 eqtrdi 
 |-  ( N = 5 -> ( |^ ` ( N / 2 ) ) = 3 )
43 42 oveq2d 
 |-  ( N = 5 -> ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ 3 ) )
44 1 43 eqtrid 
 |-  ( N = 5 -> J = ( 1 ..^ 3 ) )
45 44 eleq2d 
 |-  ( N = 5 -> ( K e. J <-> K e. ( 1 ..^ 3 ) ) )
46 45 biimpa 
 |-  ( ( N = 5 /\ K e. J ) -> K e. ( 1 ..^ 3 ) )
47 46 anim1ci 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( X e. ZZ /\ K e. ( 1 ..^ 3 ) ) )
48 minusmodnep2tmod 
 |-  ( ( X e. ZZ /\ K e. ( 1 ..^ 3 ) ) -> ( ( X - K ) mod 5 ) =/= ( ( X + ( 2 x. K ) ) mod 5 ) )
49 47 48 syl 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X - K ) mod 5 ) =/= ( ( X + ( 2 x. K ) ) mod 5 ) )
50 oveq2 
 |-  ( N = 5 -> ( ( X - K ) mod N ) = ( ( X - K ) mod 5 ) )
51 oveq2 
 |-  ( N = 5 -> ( ( X + ( 2 x. K ) ) mod N ) = ( ( X + ( 2 x. K ) ) mod 5 ) )
52 50 51 neeq12d 
 |-  ( N = 5 -> ( ( ( X - K ) mod N ) =/= ( ( X + ( 2 x. K ) ) mod N ) <-> ( ( X - K ) mod 5 ) =/= ( ( X + ( 2 x. K ) ) mod 5 ) ) )
53 52 ad2antrr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( ( X - K ) mod N ) =/= ( ( X + ( 2 x. K ) ) mod N ) <-> ( ( X - K ) mod 5 ) =/= ( ( X + ( 2 x. K ) ) mod 5 ) ) )
54 49 53 mpbird 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X - K ) mod N ) =/= ( ( X + ( 2 x. K ) ) mod N ) )
55 zcn 
 |-  ( X e. ZZ -> X e. CC )
56 55 adantl 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> X e. CC )
57 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
58 57 1 eleq2s 
 |-  ( K e. J -> K e. ZZ )
59 58 zcnd 
 |-  ( K e. J -> K e. CC )
60 59 ad2antlr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> K e. CC )
61 56 60 60 addassd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X + K ) + K ) = ( X + ( K + K ) ) )
62 60 2timesd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( 2 x. K ) = ( K + K ) )
63 62 eqcomd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( K + K ) = ( 2 x. K ) )
64 63 oveq2d 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( X + ( K + K ) ) = ( X + ( 2 x. K ) ) )
65 61 64 eqtrd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X + K ) + K ) = ( X + ( 2 x. K ) ) )
66 65 oveq1d 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( ( X + K ) + K ) mod N ) = ( ( X + ( 2 x. K ) ) mod N ) )
67 54 66 neeqtrrd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X - K ) mod N ) =/= ( ( ( X + K ) + K ) mod N ) )
68 zre 
 |-  ( X e. ZZ -> X e. RR )
69 68 adantl 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> X e. RR )
70 58 zred 
 |-  ( K e. J -> K e. RR )
71 70 ad2antlr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> K e. RR )
72 69 71 readdcld 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( X + K ) e. RR )
73 5nn 
 |-  5 e. NN
74 eleq1 
 |-  ( N = 5 -> ( N e. NN <-> 5 e. NN ) )
75 73 74 mpbiri 
 |-  ( N = 5 -> N e. NN )
76 75 nnrpd 
 |-  ( N = 5 -> N e. RR+ )
77 76 ad2antrr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> N e. RR+ )
78 modaddmod 
 |-  ( ( ( X + K ) e. RR /\ K e. RR /\ N e. RR+ ) -> ( ( ( ( X + K ) mod N ) + K ) mod N ) = ( ( ( X + K ) + K ) mod N ) )
79 72 71 77 78 syl3anc 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( ( ( X + K ) mod N ) + K ) mod N ) = ( ( ( X + K ) + K ) mod N ) )
80 67 79 neeqtrrd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X - K ) mod N ) =/= ( ( ( ( X + K ) mod N ) + K ) mod N ) )
81 80 ad2antrl 
 |-  ( ( ( ( X + K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X - K ) mod N ) =/= ( ( ( ( X + K ) mod N ) + K ) mod N ) )
82 oveq1 
 |-  ( ( ( X + K ) mod N ) = x -> ( ( ( X + K ) mod N ) + K ) = ( x + K ) )
83 82 oveq1d 
 |-  ( ( ( X + K ) mod N ) = x -> ( ( ( ( X + K ) mod N ) + K ) mod N ) = ( ( x + K ) mod N ) )
84 83 adantr 
 |-  ( ( ( ( X + K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( ( X + K ) mod N ) + K ) mod N ) = ( ( x + K ) mod N ) )
85 81 84 neeqtrd 
 |-  ( ( ( ( X + K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) )
86 85 olcd 
 |-  ( ( ( ( X + K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X + K ) mod N ) =/= x \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) )
87 86 ex 
 |-  ( ( ( X + K ) mod N ) = x -> ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + K ) mod N ) =/= x \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) ) )
88 orc 
 |-  ( ( ( X + K ) mod N ) =/= x -> ( ( ( X + K ) mod N ) =/= x \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) )
89 88 a1d 
 |-  ( ( ( X + K ) mod N ) =/= x -> ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + K ) mod N ) =/= x \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) ) )
90 87 89 pm2.61ine 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + K ) mod N ) =/= x \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) )
91 14 15 opthne 
 |-  ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. <-> ( 1 =/= 1 \/ ( ( X + K ) mod N ) =/= x ) )
92 neirr 
 |-  -. 1 =/= 1
93 92 biorfi 
 |-  ( ( ( X + K ) mod N ) =/= x <-> ( 1 =/= 1 \/ ( ( X + K ) mod N ) =/= x ) )
94 91 93 bitr4i 
 |-  ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. <-> ( ( X + K ) mod N ) =/= x )
95 94 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. <-> ( ( X + K ) mod N ) =/= x ) )
96 14 29 opthne 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 1 =/= 1 \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) )
97 92 biorfi 
 |-  ( ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) <-> ( 1 =/= 1 \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) )
98 96 97 bitr4i 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) )
99 98 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) )
100 95 99 orbi12d 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) <-> ( ( ( X + K ) mod N ) =/= x \/ ( ( X - K ) mod N ) =/= ( ( x + K ) mod N ) ) ) )
101 90 100 mpbird 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) )
102 2z 
 |-  2 e. ZZ
103 73 nnzi 
 |-  5 e. ZZ
104 2re 
 |-  2 e. RR
105 5re 
 |-  5 e. RR
106 2lt5 
 |-  2 < 5
107 104 105 106 ltleii 
 |-  2 <_ 5
108 eluz2 
 |-  ( 5 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 5 e. ZZ /\ 2 <_ 5 ) )
109 102 103 107 108 mpbir3an 
 |-  5 e. ( ZZ>= ` 2 )
110 eleq1 
 |-  ( N = 5 -> ( N e. ( ZZ>= ` 2 ) <-> 5 e. ( ZZ>= ` 2 ) ) )
111 109 110 mpbiri 
 |-  ( N = 5 -> N e. ( ZZ>= ` 2 ) )
112 111 ad2antrr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> N e. ( ZZ>= ` 2 ) )
113 simpr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> X e. ZZ )
114 1 ceilhalfelfzo1 
 |-  ( N e. NN -> ( K e. J -> K e. ( 1 ..^ N ) ) )
115 75 114 syl 
 |-  ( N = 5 -> ( K e. J -> K e. ( 1 ..^ N ) ) )
116 115 imp 
 |-  ( ( N = 5 /\ K e. J ) -> K e. ( 1 ..^ N ) )
117 116 adantr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> K e. ( 1 ..^ N ) )
118 zplusmodne 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ X e. ZZ /\ K e. ( 1 ..^ N ) ) -> ( ( X + K ) mod N ) =/= ( X mod N ) )
119 112 113 117 118 syl3anc 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X + K ) mod N ) =/= ( X mod N ) )
120 59 adantl 
 |-  ( ( N = 5 /\ K e. J ) -> K e. CC )
121 npcan 
 |-  ( ( X e. CC /\ K e. CC ) -> ( ( X - K ) + K ) = X )
122 55 120 121 syl2anr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X - K ) + K ) = X )
123 122 oveq1d 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( ( X - K ) + K ) mod N ) = ( X mod N ) )
124 119 123 neeqtrrd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X + K ) mod N ) =/= ( ( ( X - K ) + K ) mod N ) )
125 57 zred 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. RR )
126 125 1 eleq2s 
 |-  ( K e. J -> K e. RR )
127 126 ad2antlr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> K e. RR )
128 69 127 resubcld 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( X - K ) e. RR )
129 5rp 
 |-  5 e. RR+
130 eleq1 
 |-  ( N = 5 -> ( N e. RR+ <-> 5 e. RR+ ) )
131 129 130 mpbiri 
 |-  ( N = 5 -> N e. RR+ )
132 131 ad2antrr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> N e. RR+ )
133 modaddmod 
 |-  ( ( ( X - K ) e. RR /\ K e. RR /\ N e. RR+ ) -> ( ( ( ( X - K ) mod N ) + K ) mod N ) = ( ( ( X - K ) + K ) mod N ) )
134 128 127 132 133 syl3anc 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( ( ( X - K ) mod N ) + K ) mod N ) = ( ( ( X - K ) + K ) mod N ) )
135 124 134 neeqtrrd 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( ( X + K ) mod N ) =/= ( ( ( ( X - K ) mod N ) + K ) mod N ) )
136 135 ad2antrl 
 |-  ( ( ( ( X - K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X + K ) mod N ) =/= ( ( ( ( X - K ) mod N ) + K ) mod N ) )
137 oveq1 
 |-  ( ( ( X - K ) mod N ) = x -> ( ( ( X - K ) mod N ) + K ) = ( x + K ) )
138 137 oveq1d 
 |-  ( ( ( X - K ) mod N ) = x -> ( ( ( ( X - K ) mod N ) + K ) mod N ) = ( ( x + K ) mod N ) )
139 138 adantr 
 |-  ( ( ( ( X - K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( ( X - K ) mod N ) + K ) mod N ) = ( ( x + K ) mod N ) )
140 136 139 neeqtrd 
 |-  ( ( ( ( X - K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) )
141 140 orcd 
 |-  ( ( ( ( X - K ) mod N ) = x /\ ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) ) -> ( ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) \/ ( ( X - K ) mod N ) =/= x ) )
142 141 ex 
 |-  ( ( ( X - K ) mod N ) = x -> ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) \/ ( ( X - K ) mod N ) =/= x ) ) )
143 olc 
 |-  ( ( ( X - K ) mod N ) =/= x -> ( ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) \/ ( ( X - K ) mod N ) =/= x ) )
144 143 a1d 
 |-  ( ( ( X - K ) mod N ) =/= x -> ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) \/ ( ( X - K ) mod N ) =/= x ) ) )
145 142 144 pm2.61ine 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) \/ ( ( X - K ) mod N ) =/= x ) )
146 14 15 opthne 
 |-  ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 1 =/= 1 \/ ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) ) )
147 92 biorfi 
 |-  ( ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) <-> ( 1 =/= 1 \/ ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) ) )
148 146 147 bitr4i 
 |-  ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) )
149 148 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) ) )
150 14 29 opthne 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. <-> ( 1 =/= 1 \/ ( ( X - K ) mod N ) =/= x ) )
151 92 biorfi 
 |-  ( ( ( X - K ) mod N ) =/= x <-> ( 1 =/= 1 \/ ( ( X - K ) mod N ) =/= x ) )
152 150 151 bitr4i 
 |-  ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. <-> ( ( X - K ) mod N ) =/= x )
153 152 a1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. <-> ( ( X - K ) mod N ) =/= x ) )
154 149 153 orbi12d 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) <-> ( ( ( X + K ) mod N ) =/= ( ( x + K ) mod N ) \/ ( ( X - K ) mod N ) =/= x ) ) )
155 145 154 mpbird 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) )
156 opex 
 |-  <. 1 , ( ( x + K ) mod N ) >. e. _V
157 34 156 pm3.2i 
 |-  ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V )
158 7 157 pm3.2i 
 |-  ( ( <. 1 , ( ( X + K ) mod N ) >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) )
159 prneimg2 
 |-  ( ( ( <. 1 , ( ( X + K ) mod N ) >. e. _V /\ <. 1 , ( ( X - K ) mod N ) >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> ( ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) /\ ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) ) ) )
160 158 159 mp1i 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> ( ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , x >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. ) /\ ( <. 1 , ( ( X + K ) mod N ) >. =/= <. 1 , ( ( x + K ) mod N ) >. \/ <. 1 , ( ( X - K ) mod N ) >. =/= <. 1 , x >. ) ) ) )
161 101 155 160 mpbir2and 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
162 25 39 161 3jca 
 |-  ( ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) /\ x e. ( 0 ..^ N ) ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
163 162 ralrimiva 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> A. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
164 ralnex 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> -. E. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
165 3ioran 
 |-  ( -. ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
166 df-ne 
 |-  ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
167 df-ne 
 |-  ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } )
168 df-ne 
 |-  ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } )
169 166 167 168 3anbi123i 
 |-  ( ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
170 165 169 bitr4i 
 |-  ( -. ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
171 170 ralbii 
 |-  ( A. x e. ( 0 ..^ N ) -. ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
172 164 171 bitr3i 
 |-  ( -. E. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> A. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } =/= { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
173 163 172 sylibr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> -. E. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
174 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
175 eleq1 
 |-  ( N = 5 -> ( N e. ( ZZ>= ` 3 ) <-> 5 e. ( ZZ>= ` 3 ) ) )
176 174 175 mpbiri 
 |-  ( N = 5 -> N e. ( ZZ>= ` 3 ) )
177 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
178 177 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
179 176 178 sylan 
 |-  ( ( N = 5 /\ K e. J ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
180 179 adantr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } e. E <-> E. x e. ( 0 ..^ N ) ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
181 173 180 mtbird 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } e. E )
182 df-nel 
 |-  ( { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } e/ E <-> -. { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } e. E )
183 181 182 sylibr 
 |-  ( ( ( N = 5 /\ K e. J ) /\ X e. ZZ ) -> { <. 1 , ( ( X + K ) mod N ) >. , <. 1 , ( ( X - K ) mod N ) >. } e/ E )