Metamath Proof Explorer

Theorem pgnbgreunbgrlem2lem1

Description: Lemma 1 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 pgnbgreunbgrlem2lem1 
|- ( ( ( ( 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 zaddcld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y + 2 ) e. ZZ )
48 1zzd 
 |-  ( y e. ( 0 ..^ 5 ) -> 1 e. ZZ )
49 44 48 zaddcld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y + 1 ) e. ZZ )
50 5nn 
 |-  5 e. NN
51 50 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> 5 e. NN )
52 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 ) ) )
53 47 49 51 52 syl3anc 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y + 2 ) - ( y + 1 ) ) mod 5 ) = 0 <-> ( ( y + 2 ) mod 5 ) = ( ( y + 1 ) mod 5 ) ) )
54 44 zcnd 
 |-  ( y e. ( 0 ..^ 5 ) -> y e. CC )
55 2cnd 
 |-  ( y e. ( 0 ..^ 5 ) -> 2 e. CC )
56 1cnd 
 |-  ( y e. ( 0 ..^ 5 ) -> 1 e. CC )
57 54 55 56 pnpcand 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y + 2 ) - ( y + 1 ) ) = ( 2 - 1 ) )
58 2m1e1 
 |-  ( 2 - 1 ) = 1
59 57 58 eqtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y + 2 ) - ( y + 1 ) ) = 1 )
60 59 oveq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 2 ) - ( y + 1 ) ) mod 5 ) = ( 1 mod 5 ) )
61 60 eqeq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y + 2 ) - ( y + 1 ) ) mod 5 ) = 0 <-> ( 1 mod 5 ) = 0 ) )
62 43 53 61 3bitr2d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 1 ) mod 5 ) = ( ( y + 2 ) mod 5 ) <-> ( 1 mod 5 ) = 0 ) )
63 1re 
 |-  1 e. RR
64 5rp 
 |-  5 e. RR+
65 0le1 
 |-  0 <_ 1
66 1lt5 
 |-  1 < 5
67 modid 
 |-  ( ( ( 1 e. RR /\ 5 e. RR+ ) /\ ( 0 <_ 1 /\ 1 < 5 ) ) -> ( 1 mod 5 ) = 1 )
68 63 64 65 66 67 mp4an 
 |-  ( 1 mod 5 ) = 1
69 68 eqeq1i 
 |-  ( ( 1 mod 5 ) = 0 <-> 1 = 0 )
70 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
71 23 70 mpi 
 |-  ( 1 = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
72 69 71 sylbi 
 |-  ( ( 1 mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
73 62 72 biimtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y + 1 ) mod 5 ) = ( ( y + 2 ) mod 5 ) -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
74 73 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 ) )
75 41 74 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 ) )
76 75 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 ) ) )
77 39 76 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 ) ) )
78 8 16 opth 
 |-  ( <. 0 , b >. = <. 1 , ( 2nd ` <. 0 , y >. ) >. <-> ( 0 = 1 /\ b = ( 2nd ` <. 0 , y >. ) ) )
79 0ne1 
 |-  0 =/= 1
80 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 ) ) ) )
81 79 80 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 ) ) )
82 81 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 ) ) )
83 78 82 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 ) ) )
84 33 oveq1i 
 |-  ( ( 2nd ` <. 0 , y >. ) - 1 ) = ( y - 1 )
85 84 oveq1i 
 |-  ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) = ( ( y - 1 ) mod 5 )
86 85 opeq2i 
 |-  <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. = <. 0 , ( ( y - 1 ) mod 5 ) >.
87 86 eqeq2i 
 |-  ( <. 0 , b >. = <. 0 , ( ( ( 2nd ` <. 0 , y >. ) - 1 ) mod 5 ) >. <-> <. 0 , b >. = <. 0 , ( ( y - 1 ) mod 5 ) >. )
88 8 16 opth 
 |-  ( <. 0 , b >. = <. 0 , ( ( y - 1 ) mod 5 ) >. <-> ( 0 = 0 /\ b = ( ( y - 1 ) mod 5 ) ) )
89 eqeq1 
 |-  ( b = ( ( y - 1 ) mod 5 ) -> ( b = ( ( y + 2 ) mod 5 ) <-> ( ( y - 1 ) mod 5 ) = ( ( y + 2 ) mod 5 ) ) )
90 89 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 ) ) )
91 44 48 zsubcld 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y - 1 ) e. ZZ )
92 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 ) ) )
93 92 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 ) )
94 91 47 51 93 syl3anc 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y - 1 ) mod 5 ) = ( ( y + 2 ) mod 5 ) <-> ( ( ( y - 1 ) - ( y + 2 ) ) mod 5 ) = 0 ) )
95 54 56 54 55 subsubadd23 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - 1 ) - ( y + 2 ) ) = ( ( y - y ) - ( 1 + 2 ) ) )
96 54 subidd 
 |-  ( y e. ( 0 ..^ 5 ) -> ( y - y ) = 0 )
97 1p2e3 
 |-  ( 1 + 2 ) = 3
98 97 a1i 
 |-  ( y e. ( 0 ..^ 5 ) -> ( 1 + 2 ) = 3 )
99 96 98 oveq12d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - y ) - ( 1 + 2 ) ) = ( 0 - 3 ) )
100 df-neg 
 |-  -u 3 = ( 0 - 3 )
101 99 100 eqtr4di 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - y ) - ( 1 + 2 ) ) = -u 3 )
102 95 101 eqtrd 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( y - 1 ) - ( y + 2 ) ) = -u 3 )
103 102 oveq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( y - 1 ) - ( y + 2 ) ) mod 5 ) = ( -u 3 mod 5 ) )
104 103 eqeq1d 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y - 1 ) - ( y + 2 ) ) mod 5 ) = 0 <-> ( -u 3 mod 5 ) = 0 ) )
105 3re 
 |-  3 e. RR
106 negmod0 
 |-  ( ( 3 e. RR /\ 5 e. RR+ ) -> ( ( 3 mod 5 ) = 0 <-> ( -u 3 mod 5 ) = 0 ) )
107 105 64 106 mp2an 
 |-  ( ( 3 mod 5 ) = 0 <-> ( -u 3 mod 5 ) = 0 )
108 0re 
 |-  0 e. RR
109 3pos 
 |-  0 < 3
110 108 105 109 ltleii 
 |-  0 <_ 3
111 3lt5 
 |-  3 < 5
112 modid 
 |-  ( ( ( 3 e. RR /\ 5 e. RR+ ) /\ ( 0 <_ 3 /\ 3 < 5 ) ) -> ( 3 mod 5 ) = 3 )
113 105 64 110 111 112 mp4an 
 |-  ( 3 mod 5 ) = 3
114 113 eqeq1i 
 |-  ( ( 3 mod 5 ) = 0 <-> 3 = 0 )
115 3ne0 
 |-  3 =/= 0
116 eqneqall 
 |-  ( 3 = 0 -> ( 3 =/= 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
117 115 116 mpi 
 |-  ( 3 = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
118 114 117 sylbi 
 |-  ( ( 3 mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
119 107 118 sylbir 
 |-  ( ( -u 3 mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E )
120 104 119 biimtrdi 
 |-  ( y e. ( 0 ..^ 5 ) -> ( ( ( ( y - 1 ) - ( y + 2 ) ) mod 5 ) = 0 -> -. { <. 0 , b >. , <. 1 , ( ( y + 2 ) mod 5 ) >. } e. E ) )
121 94 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 90 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 88 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 87 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 77 83 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 )