Metamath Proof Explorer

Theorem gpg5edgnedg

Description: Two consecutive (according to the numbering) inside vertices of the Petersen graph G(5,2) are not connected by an edge, but are connected by an edge in a 5-prism G(5,1). (Contributed by AV, 29-Dec-2025)

Ref Expression
Assertion gpg5edgnedg 
|- ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) )

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 eleq1 
 |-  ( x = 0 -> ( x e. ( 0 ..^ 5 ) <-> 0 e. ( 0 ..^ 5 ) ) )
3 opeq2 
 |-  ( x = 0 -> <. 0 , x >. = <. 0 , 0 >. )
4 oveq1 
 |-  ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
5 4 oveq1d 
 |-  ( x = 0 -> ( ( x + 1 ) mod 5 ) = ( ( 0 + 1 ) mod 5 ) )
6 5 opeq2d 
 |-  ( x = 0 -> <. 0 , ( ( x + 1 ) mod 5 ) >. = <. 0 , ( ( 0 + 1 ) mod 5 ) >. )
7 3 6 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod 5 ) >. } )
8 7 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } <-> { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod 5 ) >. } ) )
9 opeq2 
 |-  ( x = 0 -> <. 1 , x >. = <. 1 , 0 >. )
10 3 9 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , 0 >. , <. 1 , 0 >. } )
11 10 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
12 5 opeq2d 
 |-  ( x = 0 -> <. 1 , ( ( x + 1 ) mod 5 ) >. = <. 1 , ( ( 0 + 1 ) mod 5 ) >. )
13 9 12 preq12d 
 |-  ( x = 0 -> { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod 5 ) >. } )
14 13 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } <-> { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod 5 ) >. } ) )
15 8 11 14 3orbi123d 
 |-  ( x = 0 -> ( ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod 5 ) >. } ) ) )
16 2 15 anbi12d 
 |-  ( x = 0 -> ( ( x e. ( 0 ..^ 5 ) /\ ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } ) ) <-> ( 0 e. ( 0 ..^ 5 ) /\ ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod 5 ) >. } ) ) ) )
17 5nn 
 |-  5 e. NN
18 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 5 ) <-> 5 e. NN )
19 17 18 mpbir 
 |-  0 e. ( 0 ..^ 5 )
20 0p1e1 
 |-  ( 0 + 1 ) = 1
21 20 oveq1i 
 |-  ( ( 0 + 1 ) mod 5 ) = ( 1 mod 5 )
22 5re 
 |-  5 e. RR
23 1lt5 
 |-  1 < 5
24 1mod 
 |-  ( ( 5 e. RR /\ 1 < 5 ) -> ( 1 mod 5 ) = 1 )
25 22 23 24 mp2an 
 |-  ( 1 mod 5 ) = 1
26 21 25 eqtr2i 
 |-  1 = ( ( 0 + 1 ) mod 5 )
27 26 opeq2i 
 |-  <. 1 , 1 >. = <. 1 , ( ( 0 + 1 ) mod 5 ) >.
28 27 preq2i 
 |-  { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod 5 ) >. }
29 28 3mix3i 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod 5 ) >. } )
30 19 29 pm3.2i 
 |-  ( 0 e. ( 0 ..^ 5 ) /\ ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod 5 ) >. } ) )
31 1 16 30 ceqsexv2d 
 |-  E. x ( x e. ( 0 ..^ 5 ) /\ ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } ) )
32 df-rex 
 |-  ( E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } ) <-> E. x ( x e. ( 0 ..^ 5 ) /\ ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } ) ) )
33 31 32 mpbir 
 |-  E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } )
34 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
35 2z 
 |-  2 e. ZZ
36 22 rehalfcli 
 |-  ( 5 / 2 ) e. RR
37 ceilcl 
 |-  ( ( 5 / 2 ) e. RR -> ( |^ ` ( 5 / 2 ) ) e. ZZ )
38 36 37 ax-mp 
 |-  ( |^ ` ( 5 / 2 ) ) e. ZZ
39 2ltceilhalf 
 |-  ( 5 e. ( ZZ>= ` 3 ) -> 2 <_ ( |^ ` ( 5 / 2 ) ) )
40 34 39 ax-mp 
 |-  2 <_ ( |^ ` ( 5 / 2 ) )
41 eluz2 
 |-  ( ( |^ ` ( 5 / 2 ) ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( |^ ` ( 5 / 2 ) ) e. ZZ /\ 2 <_ ( |^ ` ( 5 / 2 ) ) ) )
42 35 38 40 41 mpbir3an 
 |-  ( |^ ` ( 5 / 2 ) ) e. ( ZZ>= ` 2 )
43 fzo1lb 
 |-  ( 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) <-> ( |^ ` ( 5 / 2 ) ) e. ( ZZ>= ` 2 ) )
44 42 43 mpbir 
 |-  1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
45 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
46 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
47 eqid 
 |-  ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
48 eqid 
 |-  ( Edg ` ( 5 gPetersenGr 1 ) ) = ( Edg ` ( 5 gPetersenGr 1 ) )
49 45 46 47 48 gpgedgel 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } ) ) )
50 34 44 49 mp2an 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod 5 ) >. } ) )
51 33 50 mpbir 
 |-  { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) )
52 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
53 opex 
 |-  <. 1 , 0 >. e. _V
54 opex 
 |-  <. 1 , 1 >. e. _V
55 53 54 pm3.2i 
 |-  ( <. 1 , 0 >. e. _V /\ <. 1 , 1 >. e. _V )
56 opex 
 |-  <. 0 , x >. e. _V
57 opex 
 |-  <. 0 , ( ( x + 1 ) mod 5 ) >. e. _V
58 56 57 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod 5 ) >. e. _V )
59 55 58 pm3.2i 
 |-  ( ( <. 1 , 0 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod 5 ) >. e. _V ) )
60 ax-1ne0 
 |-  1 =/= 0
61 60 orci 
 |-  ( 1 =/= 0 \/ 0 =/= x )
62 1ex 
 |-  1 e. _V
63 62 1 opthne 
 |-  ( <. 1 , 0 >. =/= <. 0 , x >. <-> ( 1 =/= 0 \/ 0 =/= x ) )
64 61 63 mpbir 
 |-  <. 1 , 0 >. =/= <. 0 , x >.
65 60 orci 
 |-  ( 1 =/= 0 \/ 0 =/= ( ( x + 1 ) mod 5 ) )
66 62 1 opthne 
 |-  ( <. 1 , 0 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >. <-> ( 1 =/= 0 \/ 0 =/= ( ( x + 1 ) mod 5 ) ) )
67 65 66 mpbir 
 |-  <. 1 , 0 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >.
68 64 67 pm3.2i 
 |-  ( <. 1 , 0 >. =/= <. 0 , x >. /\ <. 1 , 0 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >. )
69 68 a1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 0 >. =/= <. 0 , x >. /\ <. 1 , 0 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >. ) )
70 69 orcd 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( ( <. 1 , 0 >. =/= <. 0 , x >. /\ <. 1 , 0 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >. ) \/ ( <. 1 , 1 >. =/= <. 0 , x >. /\ <. 1 , 1 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >. ) ) )
71 prneimg 
 |-  ( ( ( <. 1 , 0 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod 5 ) >. e. _V ) ) -> ( ( ( <. 1 , 0 >. =/= <. 0 , x >. /\ <. 1 , 0 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >. ) \/ ( <. 1 , 1 >. =/= <. 0 , x >. /\ <. 1 , 1 >. =/= <. 0 , ( ( x + 1 ) mod 5 ) >. ) ) -> { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } ) )
72 59 70 71 mpsyl 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } )
73 64 orci 
 |-  ( <. 1 , 0 >. =/= <. 0 , x >. \/ <. 1 , 1 >. =/= <. 1 , x >. )
74 73 a1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 0 >. =/= <. 0 , x >. \/ <. 1 , 1 >. =/= <. 1 , x >. ) )
75 60 orci 
 |-  ( 1 =/= 0 \/ 1 =/= x )
76 62 62 opthne 
 |-  ( <. 1 , 1 >. =/= <. 0 , x >. <-> ( 1 =/= 0 \/ 1 =/= x ) )
77 75 76 mpbir 
 |-  <. 1 , 1 >. =/= <. 0 , x >.
78 77 olci 
 |-  ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 0 , x >. )
79 78 a1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 0 , x >. ) )
80 opex 
 |-  <. 1 , x >. e. _V
81 56 80 pm3.2i 
 |-  ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V )
82 55 81 pm3.2i 
 |-  ( ( <. 1 , 0 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) )
83 prneimg2 
 |-  ( ( ( <. 1 , 0 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) ) -> ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 1 , 0 >. =/= <. 0 , x >. \/ <. 1 , 1 >. =/= <. 1 , x >. ) /\ ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 0 , x >. ) ) ) )
84 82 83 mp1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> ( ( <. 1 , 0 >. =/= <. 0 , x >. \/ <. 1 , 1 >. =/= <. 1 , x >. ) /\ ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 0 , x >. ) ) ) )
85 74 79 84 mpbir2and 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } )
86 1ne2 
 |-  1 =/= 2
87 86 a1i 
 |-  ( ( 0 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> 1 =/= 2 )
88 2cn 
 |-  2 e. CC
89 88 addlidi 
 |-  ( 0 + 2 ) = 2
90 89 oveq1i 
 |-  ( ( 0 + 2 ) mod 5 ) = ( 2 mod 5 )
91 2nn0 
 |-  2 e. NN0
92 2lt5 
 |-  2 < 5
93 elfzo0 
 |-  ( 2 e. ( 0 ..^ 5 ) <-> ( 2 e. NN0 /\ 5 e. NN /\ 2 < 5 ) )
94 91 17 92 93 mpbir3an 
 |-  2 e. ( 0 ..^ 5 )
95 zmodidfzoimp 
 |-  ( 2 e. ( 0 ..^ 5 ) -> ( 2 mod 5 ) = 2 )
96 94 95 ax-mp 
 |-  ( 2 mod 5 ) = 2
97 90 96 eqtr2i 
 |-  2 = ( ( 0 + 2 ) mod 5 )
98 oveq1 
 |-  ( 0 = x -> ( 0 + 2 ) = ( x + 2 ) )
99 98 oveq1d 
 |-  ( 0 = x -> ( ( 0 + 2 ) mod 5 ) = ( ( x + 2 ) mod 5 ) )
100 97 99 eqtrid 
 |-  ( 0 = x -> 2 = ( ( x + 2 ) mod 5 ) )
101 100 adantr 
 |-  ( ( 0 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> 2 = ( ( x + 2 ) mod 5 ) )
102 87 101 neeqtrd 
 |-  ( ( 0 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> 1 =/= ( ( x + 2 ) mod 5 ) )
103 102 olcd 
 |-  ( ( 0 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> ( 0 =/= x \/ 1 =/= ( ( x + 2 ) mod 5 ) ) )
104 103 ex 
 |-  ( 0 = x -> ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( 0 =/= x \/ 1 =/= ( ( x + 2 ) mod 5 ) ) ) )
105 orc 
 |-  ( 0 =/= x -> ( 0 =/= x \/ 1 =/= ( ( x + 2 ) mod 5 ) ) )
106 105 a1d 
 |-  ( 0 =/= x -> ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( 0 =/= x \/ 1 =/= ( ( x + 2 ) mod 5 ) ) ) )
107 104 106 pm2.61ine 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( 0 =/= x \/ 1 =/= ( ( x + 2 ) mod 5 ) ) )
108 62 1 opthne 
 |-  ( <. 1 , 0 >. =/= <. 1 , x >. <-> ( 1 =/= 1 \/ 0 =/= x ) )
109 neirr 
 |-  -. 1 =/= 1
110 109 biorfi 
 |-  ( 0 =/= x <-> ( 1 =/= 1 \/ 0 =/= x ) )
111 108 110 bitr4i 
 |-  ( <. 1 , 0 >. =/= <. 1 , x >. <-> 0 =/= x )
112 111 a1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 0 >. =/= <. 1 , x >. <-> 0 =/= x ) )
113 62 62 opthne 
 |-  ( <. 1 , 1 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. <-> ( 1 =/= 1 \/ 1 =/= ( ( x + 2 ) mod 5 ) ) )
114 109 biorfi 
 |-  ( 1 =/= ( ( x + 2 ) mod 5 ) <-> ( 1 =/= 1 \/ 1 =/= ( ( x + 2 ) mod 5 ) ) )
115 113 114 bitr4i 
 |-  ( <. 1 , 1 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. <-> 1 =/= ( ( x + 2 ) mod 5 ) )
116 115 a1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 1 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. <-> 1 =/= ( ( x + 2 ) mod 5 ) ) )
117 112 116 orbi12d 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. ) <-> ( 0 =/= x \/ 1 =/= ( ( x + 2 ) mod 5 ) ) ) )
118 107 117 mpbird 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. ) )
119 0re 
 |-  0 e. RR
120 3pos 
 |-  0 < 3
121 119 120 ltneii 
 |-  0 =/= 3
122 121 a1i 
 |-  ( ( 1 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> 0 =/= 3 )
123 1p2e3 
 |-  ( 1 + 2 ) = 3
124 123 oveq1i 
 |-  ( ( 1 + 2 ) mod 5 ) = ( 3 mod 5 )
125 3nn0 
 |-  3 e. NN0
126 3lt5 
 |-  3 < 5
127 elfzo0 
 |-  ( 3 e. ( 0 ..^ 5 ) <-> ( 3 e. NN0 /\ 5 e. NN /\ 3 < 5 ) )
128 125 17 126 127 mpbir3an 
 |-  3 e. ( 0 ..^ 5 )
129 zmodidfzoimp 
 |-  ( 3 e. ( 0 ..^ 5 ) -> ( 3 mod 5 ) = 3 )
130 128 129 ax-mp 
 |-  ( 3 mod 5 ) = 3
131 124 130 eqtr2i 
 |-  3 = ( ( 1 + 2 ) mod 5 )
132 oveq1 
 |-  ( 1 = x -> ( 1 + 2 ) = ( x + 2 ) )
133 132 oveq1d 
 |-  ( 1 = x -> ( ( 1 + 2 ) mod 5 ) = ( ( x + 2 ) mod 5 ) )
134 131 133 eqtrid 
 |-  ( 1 = x -> 3 = ( ( x + 2 ) mod 5 ) )
135 134 adantr 
 |-  ( ( 1 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> 3 = ( ( x + 2 ) mod 5 ) )
136 122 135 neeqtrd 
 |-  ( ( 1 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> 0 =/= ( ( x + 2 ) mod 5 ) )
137 136 orcd 
 |-  ( ( 1 = x /\ ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) ) -> ( 0 =/= ( ( x + 2 ) mod 5 ) \/ 1 =/= x ) )
138 137 ex 
 |-  ( 1 = x -> ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( 0 =/= ( ( x + 2 ) mod 5 ) \/ 1 =/= x ) ) )
139 olc 
 |-  ( 1 =/= x -> ( 0 =/= ( ( x + 2 ) mod 5 ) \/ 1 =/= x ) )
140 139 a1d 
 |-  ( 1 =/= x -> ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( 0 =/= ( ( x + 2 ) mod 5 ) \/ 1 =/= x ) ) )
141 138 140 pm2.61ine 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( 0 =/= ( ( x + 2 ) mod 5 ) \/ 1 =/= x ) )
142 62 1 opthne 
 |-  ( <. 1 , 0 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. <-> ( 1 =/= 1 \/ 0 =/= ( ( x + 2 ) mod 5 ) ) )
143 109 biorfi 
 |-  ( 0 =/= ( ( x + 2 ) mod 5 ) <-> ( 1 =/= 1 \/ 0 =/= ( ( x + 2 ) mod 5 ) ) )
144 142 143 bitr4i 
 |-  ( <. 1 , 0 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. <-> 0 =/= ( ( x + 2 ) mod 5 ) )
145 144 a1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 0 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. <-> 0 =/= ( ( x + 2 ) mod 5 ) ) )
146 62 62 opthne 
 |-  ( <. 1 , 1 >. =/= <. 1 , x >. <-> ( 1 =/= 1 \/ 1 =/= x ) )
147 109 biorfi 
 |-  ( 1 =/= x <-> ( 1 =/= 1 \/ 1 =/= x ) )
148 146 147 bitr4i 
 |-  ( <. 1 , 1 >. =/= <. 1 , x >. <-> 1 =/= x )
149 148 a1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 1 >. =/= <. 1 , x >. <-> 1 =/= x ) )
150 145 149 orbi12d 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( ( <. 1 , 0 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. \/ <. 1 , 1 >. =/= <. 1 , x >. ) <-> ( 0 =/= ( ( x + 2 ) mod 5 ) \/ 1 =/= x ) ) )
151 141 150 mpbird 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( <. 1 , 0 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. \/ <. 1 , 1 >. =/= <. 1 , x >. ) )
152 opex 
 |-  <. 1 , ( ( x + 2 ) mod 5 ) >. e. _V
153 80 152 pm3.2i 
 |-  ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + 2 ) mod 5 ) >. e. _V )
154 55 153 pm3.2i 
 |-  ( ( <. 1 , 0 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + 2 ) mod 5 ) >. e. _V ) )
155 prneimg2 
 |-  ( ( ( <. 1 , 0 >. e. _V /\ <. 1 , 1 >. e. _V ) /\ ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + 2 ) mod 5 ) >. e. _V ) ) -> ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } <-> ( ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. ) /\ ( <. 1 , 0 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. \/ <. 1 , 1 >. =/= <. 1 , x >. ) ) ) )
156 154 155 mp1i 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } <-> ( ( <. 1 , 0 >. =/= <. 1 , x >. \/ <. 1 , 1 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. ) /\ ( <. 1 , 0 >. =/= <. 1 , ( ( x + 2 ) mod 5 ) >. \/ <. 1 , 1 >. =/= <. 1 , x >. ) ) ) )
157 118 151 156 mpbir2and 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } )
158 72 85 157 3jca 
 |-  ( ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) /\ x e. ( 0 ..^ 5 ) ) -> ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
159 158 ralrimiva 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> A. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
160 ralnex 
 |-  ( A. x e. ( 0 ..^ 5 ) -. ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) <-> -. E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
161 3ioran 
 |-  ( -. ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) <-> ( -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
162 df-ne 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } <-> -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } )
163 df-ne 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } <-> -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } )
164 df-ne 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } <-> -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } )
165 162 163 164 3anbi123i 
 |-  ( ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) <-> ( -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } /\ -. { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
166 161 165 bitr4i 
 |-  ( -. ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
167 166 ralbii 
 |-  ( A. x e. ( 0 ..^ 5 ) -. ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) <-> A. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
168 160 167 bitr3i 
 |-  ( -. E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) <-> A. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 0 , x >. , <. 1 , x >. } /\ { <. 1 , 0 >. , <. 1 , 1 >. } =/= { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
169 159 168 sylibr 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> -. E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) )
170 eqid 
 |-  ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
171 eqid 
 |-  ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) )
172 45 46 170 171 gpgedgel 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 2 ) ) <-> E. x e. ( 0 ..^ 5 ) ( { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod 5 ) >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 2 ) mod 5 ) >. } ) ) )
173 169 172 mtbird 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> -. { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 2 ) ) )
174 34 52 173 mp2an 
 |-  -. { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 2 ) )
175 174 nelir 
 |-  { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) )
176 51 175 pm3.2i 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) )