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	Could not format assertion : No typesetting found for |- ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) with typecode |-

Proof

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