Metamath Proof Explorer

Theorem pgnbgreunbgrlem2lem2

Description: Lemma 2 for pgnbgreunbgrlem2 . (Contributed by AV, 16-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g 
|- G = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v 
|- V = ( Vtx ` G )
pgnbgreunbgr.e 
|- E = ( Edg ` G )
pgnbgreunbgr.n 
|- N = ( G NeighbVtx X )
Assertion pgnbgreunbgrlem2lem2 
|- ( ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , L } e. E )

Proof

Step Hyp Ref Expression
1 pgnbgreunbgr.g 
 |-  G = ( 5 gPetersenGr 2 )
2 pgnbgreunbgr.v 
 |-  V = ( Vtx ` G )
3 pgnbgreunbgr.e 
 |-  E = ( Edg ` G )
4 pgnbgreunbgr.n 
 |-  N = ( G NeighbVtx X )
5 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
6 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
7 5 6 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
8 c0ex 
 |-  0 e. _V
9 vex 
 |-  y e. _V
10 8 9 op1st 
 |-  ( 1st ` <. 0 , y >. ) = 0
11 simpr 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ { <. 0 , y >. , <. 0 , b >. } e. E ) -> { <. 0 , y >. , <. 0 , b >. } e. E )
12 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
13 12 1 2 3 gpgvtxedg0 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( 1st ` <. 0 , y >. ) = 0 /\ { <. 0 , y >. , <. 0 , b >. } e. E ) -> ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) )
14 7 10 11 13 mp3an12i 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ { <. 0 , y >. , <. 0 , b >. } e. E ) -> ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) )
15 14 ex 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , y >. , <. 0 , b >. } e. E -> ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) )
16 vex 
 |-  b e. _V
17 8 16 op1st 
 |-  ( 1st ` <. 0 , b >. ) = 0
18 12 1 2 3 gpgvtxedg0 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ ( 1st ` <. 0 , b >. ) = 0 /\ { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) -> ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) )
19 7 17 18 mp3an12 
 |-  ( { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E -> ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) )
20 1ex 
 |-  1 e. _V
21 ovex 
 |-  ( ( y - 2 ) mod 5 ) e. _V
22 20 21 opth 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. <-> ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) ) )
23 ax-1ne0 
 |-  1 =/= 0
24 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
25 23 24 mpi 
 |-  ( 1 = 0 -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
26 25 adantr 
 |-  ( ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
27 22 26 sylbi 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
28 20 21 opth 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. <-> ( 1 = 1 /\ ( ( y - 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) ) )
29 8 16 op2nd 
 |-  ( 2nd ` <. 0 , b >. ) = b
30 29 eqeq2i 
 |-  ( ( ( y - 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) <-> ( ( y - 2 ) mod 5 ) = b )
31 eqcom 
 |-  ( ( ( y - 2 ) mod 5 ) = b <-> b = ( ( y - 2 ) mod 5 ) )
32 30 31 bitri 
 |-  ( ( ( y - 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) <-> b = ( ( y - 2 ) mod 5 ) )
33 8 9 op2nd 
 |-  ( 2nd ` <. 0 , y >. ) = y
34 33 oveq1i 
 |-  ( ( 2nd ` <. 0 , y >. ) + 1 ) = ( y + 1 )
35 34 oveq1i 
 |-  ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) = ( ( y + 1 ) mod 5 )
36 35 opeq2i 
 |-  <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. = <. 0 , ( ( y + 1 ) mod 5 ) >.
37 36 eqeq2i 
 |-  ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. <-> <. 0 , b >. = <. 0 , ( ( y + 1 ) mod 5 ) >. )
38 8 16 opth 
 |-  ( <. 0 , b >. = <. 0 , ( ( y + 1 ) mod 5 ) >. <-> ( 0 = 0 /\ b = ( ( y + 1 ) mod 5 ) ) )
39 37 38 bitri 
 |-  ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. <-> ( 0 = 0 /\ b = ( ( y + 1 ) mod 5 ) ) )
40 eqeq1 
 |-  ( b = ( ( y + 1 ) mod 5 ) -> ( b = ( ( y - 2 ) mod 5 ) <-> ( ( y + 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
41 40 adantr 
 |-  ( ( b = ( ( y + 1 ) mod 5 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( b = ( ( y - 2 ) mod 5 ) <-> ( ( y + 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
42 eqcom 
 |-  ( ( ( y + 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) <-> ( ( y - 2 ) mod 5 ) = ( ( y + 1 ) mod 5 ) )
43 42 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) <-> ( ( y - 2 ) mod 5 ) = ( ( y + 1 ) mod 5 ) ) )
44 elfzoelz 
 |-  ( y e. ( 0 ..^ 5 ) -> y e. ZZ )
45 2z 
 |-  2 e. ZZ
46 45 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> 2 e. ZZ )
47 44 46 zsubcld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y - 2 ) e. ZZ )
48 44 peano2zd 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y + 1 ) e. ZZ )
49 5nn 
 |-  5 e. NN
50 49 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> 5 e. NN )
51 difmod0 
 |-  ( ( ( y - 2 ) e. ZZ /\ ( y + 1 ) e. ZZ /\ 5 e. NN ) -> ( ( ( ( y - 2 ) - ( y + 1 ) ) mod 5 ) = 0 <-> ( ( y - 2 ) mod 5 ) = ( ( y + 1 ) mod 5 ) ) )
52 47 48 50 51 syl3anc 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y - 2 ) - ( y + 1 ) ) mod 5 ) = 0 <-> ( ( y - 2 ) mod 5 ) = ( ( y + 1 ) mod 5 ) ) )
53 44 zcnd 
 |-  ( y e. ( 0 ..^ 5 ) -> y e. CC )
54 2cnd 
 |-  ( y e. ( 0 ..^ 5 ) -> 2 e. CC )
55 1cnd 
 |-  ( y e. ( 0 ..^ 5 ) -> 1 e. CC )
56 53 54 53 55 subsubadd23 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - 2 ) - ( y + 1 ) ) = ( ( y - y ) - ( 2 + 1 ) ) )
57 53 subidd 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y - y ) = 0 )
58 2p1e3 
 |-  ( 2 + 1 ) = 3
59 58 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> ( 2 + 1 ) = 3 )
60 57 59 oveq12d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - y ) - ( 2 + 1 ) ) = ( 0 - 3 ) )
61 df-neg 
 |-  -u 3 = ( 0 - 3 )
62 60 61 eqtr4di 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - y ) - ( 2 + 1 ) ) = -u 3 )
63 56 62 eqtrd 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - 2 ) - ( y + 1 ) ) = -u 3 )
64 63 oveq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y - 2 ) - ( y + 1 ) ) mod 5 ) = ( -u 3 mod 5 ) )
65 64 eqeq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y - 2 ) - ( y + 1 ) ) mod 5 ) = 0 <-> ( -u 3 mod 5 ) = 0 ) )
66 43 52 65 3bitr2d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) <-> ( -u 3 mod 5 ) = 0 ) )
67 3re 
 |-  3 e. RR
68 5rp 
 |-  5 e. RR+
69 negmod0 
 |-  ( ( 3 e. RR /\ 5 e. RR+ ) -> ( ( 3 mod 5 ) = 0 <-> ( -u 3 mod 5 ) = 0 ) )
70 67 68 69 mp2an 
 |-  ( ( 3 mod 5 ) = 0 <-> ( -u 3 mod 5 ) = 0 )
71 0re 
 |-  0 e. RR
72 3pos 
 |-  0 < 3
73 71 67 72 ltleii 
 |-  0 <_ 3
74 3lt5 
 |-  3 < 5
75 modid 
 |-  ( ( ( 3 e. RR /\ 5 e. RR+ ) /\ ( 0 <_ 3 /\ 3 < 5 ) ) -> ( 3 mod 5 ) = 3 )
76 67 68 73 74 75 mp4an 
 |-  ( 3 mod 5 ) = 3
77 76 eqeq1i 
 |-  ( ( 3 mod 5 ) = 0 <-> 3 = 0 )
78 70 77 bitr3i 
 |-  ( ( -u 3 mod 5 ) = 0 <-> 3 = 0 )
79 3ne0 
 |-  3 =/= 0
80 eqneqall 
 |-  ( 3 = 0 -> ( 3 =/= 0 -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
81 79 80 mpi 
 |-  ( 3 = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E )
82 78 81 sylbi 
 |-  ( ( -u 3 mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E )
83 66 82 biimtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
84 83 ad2antll 
 |-  ( ( b = ( ( y + 1 ) mod 5 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( ( y + 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
85 41 84 sylbid 
 |-  ( ( b = ( ( y + 1 ) mod 5 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
86 85 ex 
 |-  ( b = ( ( y + 1 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
87 39 86 simplbiim 
 |-  ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
88 8 16 opth 
 |-  ( <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. <-> ( 0 = 1 /\ b = ( 2nd ` <. 0 , y >. ) ) )
89 0ne1 
 |-  0 =/= 1
90 eqneqall 
 |-  ( 0 = 1 -> ( 0 =/= 1 -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) ) )
91 89 90 mpi 
 |-  ( 0 = 1 -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
92 91 adantr 
 |-  ( ( 0 = 1 /\ b = ( 2nd ` <. 0 , y >. ) ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
93 88 92 sylbi 
 |-  ( <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
94 33 oveq1i 
 |-  ( ( 2nd ` <. 0 , y >. ) - 1 ) = ( y - 1 )
95 94 oveq1i 
 |-  ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) = ( ( y - 1 ) mod 5 )
96 95 opeq2i 
 |-  <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. = <. 0 , ( ( y - 1 ) mod 5 ) >.
97 96 eqeq2i 
 |-  ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. <-> <. 0 , b >. = <. 0 , ( ( y - 1 ) mod 5 ) >. )
98 8 16 opth 
 |-  ( <. 0 , b >. = <. 0 , ( ( y - 1 ) mod 5 ) >. <-> ( 0 = 0 /\ b = ( ( y - 1 ) mod 5 ) ) )
99 eqeq1 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> ( b = ( ( y - 2 ) mod 5 ) <-> ( ( y - 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
100 99 adantr 
 |-  ( ( b = ( ( y - 1 ) mod 5 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( b = ( ( y - 2 ) mod 5 ) <-> ( ( y - 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
101 1zzd 
 |-  ( y e. ( 0 ..^ 5 ) -> 1 e. ZZ )
102 44 101 zsubcld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y - 1 ) e. ZZ )
103 difmod0 
 |-  ( ( ( y - 1 ) e. ZZ /\ ( y - 2 ) e. ZZ /\ 5 e. NN ) -> ( ( ( ( y - 1 ) - ( y - 2 ) ) mod 5 ) = 0 <-> ( ( y - 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) ) )
104 103 bicomd 
 |-  ( ( ( y - 1 ) e. ZZ /\ ( y - 2 ) e. ZZ /\ 5 e. NN ) -> ( ( ( y - 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) <-> ( ( ( y - 1 ) - ( y - 2 ) ) mod 5 ) = 0 ) )
105 102 47 50 104 syl3anc 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y - 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) <-> ( ( ( y - 1 ) - ( y - 2 ) ) mod 5 ) = 0 ) )
106 53 55 54 nnncan1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - 1 ) - ( y - 2 ) ) = ( 2 - 1 ) )
107 2m1e1 
 |-  ( 2 - 1 ) = 1
108 106 107 eqtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - 1 ) - ( y - 2 ) ) = 1 )
109 108 oveq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y - 1 ) - ( y - 2 ) ) mod 5 ) = ( 1 mod 5 ) )
110 109 eqeq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y - 1 ) - ( y - 2 ) ) mod 5 ) = 0 <-> ( 1 mod 5 ) = 0 ) )
111 1re 
 |-  1 e. RR
112 0le1 
 |-  0 <_ 1
113 1lt5 
 |-  1 < 5
114 modid 
 |-  ( ( ( 1 e. RR /\ 5 e. RR+ ) /\ ( 0 <_ 1 /\ 1 < 5 ) ) -> ( 1 mod 5 ) = 1 )
115 111 68 112 113 114 mp4an 
 |-  ( 1 mod 5 ) = 1
116 115 eqeq1i 
 |-  ( ( 1 mod 5 ) = 0 <-> 1 = 0 )
117 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
118 23 117 mpi 
 |-  ( 1 = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E )
119 116 118 sylbi 
 |-  ( ( 1 mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E )
120 110 119 biimtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y - 1 ) - ( y - 2 ) ) mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
121 105 120 sylbid 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y - 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
122 121 ad2antll 
 |-  ( ( b = ( ( y - 1 ) mod 5 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( ( y - 1 ) mod 5 ) = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
123 100 122 sylbid 
 |-  ( ( b = ( ( y - 1 ) mod 5 ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
124 123 ex 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
125 98 124 simplbiim 
 |-  ( <. 0 , b >. = <. 0 , ( ( y - 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
126 97 125 sylbi 
 |-  ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
127 87 93 126 3jaoi 
 |-  ( ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( b = ( ( y - 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
128 127 com13 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
129 128 impd 
 |-  ( b = ( ( y - 2 ) mod 5 ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
130 32 129 sylbi 
 |-  ( ( ( y - 2 ) mod 5 ) = ( 2nd ` <. 0 , b >. ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
131 28 130 simplbiim 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
132 20 21 opth 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. <-> ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) ) )
133 25 adantr 
 |-  ( ( 1 = 0 /\ ( ( y - 2 ) mod 5 ) = ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
134 132 133 sylbi 
 |-  ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
135 27 131 134 3jaoi 
 |-  ( ( <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) + 1 ) mod 5 ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 1 , ( 2nd ` <. 0 , b >. ) >. \/ <. 1 , ( ( y - 2 ) mod 5 ) >. = <. 0 , ( ( ( 2nd ` <. 0 , b >. ) - 1 ) mod 5 ) >. ) -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
136 19 135 syl 
 |-  ( { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
137 ax-1 
 |-  ( -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E -> ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
138 136 137 pm2.61i 
 |-  ( ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) /\ ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E )
139 138 ex 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) + 1 ) mod 5 ) >. \/ <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. \/ <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. ) -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
140 15 139 syld 
 |-  ( ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) -> ( { <. 0 , y >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
141 140 adantl 
 |-  ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { <. 0 , y >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
142 preq1 
 |-  ( K = <. 0 , y >. -> { K , <. 0 , b >. } = { <. 0 , y >. , <. 0 , b >. } )
143 142 eleq1d 
 |-  ( K = <. 0 , y >. -> ( { K , <. 0 , b >. } e. E <-> { <. 0 , y >. , <. 0 , b >. } e. E ) )
144 143 adantl 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( { K , <. 0 , b >. } e. E <-> { <. 0 , y >. , <. 0 , b >. } e. E ) )
145 preq2 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> { <. 0 , b >. , L } = { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } )
146 145 eleq1d 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( { <. 0 , b >. , L } e. E <-> { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
147 146 notbid 
 |-  ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. -> ( -. { <. 0 , b >. , L } e. E <-> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
148 147 adantr 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( -. { <. 0 , b >. , L } e. E <-> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) )
149 144 148 imbi12d 
 |-  ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) -> ( ( { K , <. 0 , b >. } e. E -> -. { <. 0 , b >. , L } e. E ) <-> ( { <. 0 , y >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
150 149 adantr 
 |-  ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( ( { K , <. 0 , b >. } e. E -> -. { <. 0 , b >. , L } e. E ) <-> ( { <. 0 , y >. , <. 0 , b >. } e. E -> -. { <. 0 , b >. , <. 1 , ( ( y - 2 ) mod 5 ) >. } e. E ) ) )
151 141 150 mpbird 
 |-  ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) -> ( { K , <. 0 , b >. } e. E -> -. { <. 0 , b >. , L } e. E ) )
152 151 imp 
 |-  ( ( ( ( L = <. 1 , ( ( y - 2 ) mod 5 ) >. /\ K = <. 0 , y >. ) /\ ( b e. ( 0 ..^ 5 ) /\ y e. ( 0 ..^ 5 ) ) ) /\ { K , <. 0 , b >. } e. E ) -> -. { <. 0 , b >. , L } e. E )