pgnbgreunbgrlem1

	Ref	Expression
Hypotheses	pgnbgreunbgr.g	No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
	pgnbgreunbgr.v	$⊢ V = Vtx (G)$
	pgnbgreunbgr.e	$⊢ E = Edg (G)$
	pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
Assertion	pgnbgreunbgrlem1	$⊢ (L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \to ((K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \to ((X \in V \land X = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$

Proof

Step	Hyp	Ref	Expression
1		pgnbgreunbgr.g	Could not format G = ( 5 gPetersenGr 2 ) : No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
2		pgnbgreunbgr.v	$⊢ V = Vtx (G)$
3		pgnbgreunbgr.e	$⊢ E = Edg (G)$
4		pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
5		c0ex	$⊢ 0 \in V$
6		vex	$⊢ y \in V$
7	5 6	op2ndd	$⊢ X = ⟨0, y⟩ \to 2^{nd} (X) = y$
8		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) + 1 = y + 1$
9	8	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) + 1) \mod 5 = (y + 1) \mod 5$
10	9	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨0, (2^{nd} (X) + 1) \mod 5⟩ = ⟨0, (y + 1) \mod 5⟩$
11	10	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \leftrightarrow L = ⟨0, (y + 1) \mod 5⟩)$
12		opeq2	$⊢ 2^{nd} (X) = y \to ⟨1, 2^{nd} (X)⟩ = ⟨1, y⟩$
13	12	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨1, 2^{nd} (X)⟩ \leftrightarrow L = ⟨1, y⟩)$
14		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) - 1 = y - 1$
15	14	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) - 1) \mod 5 = (y - 1) \mod 5$
16	15	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨0, (2^{nd} (X) - 1) \mod 5⟩ = ⟨0, (y - 1) \mod 5⟩$
17	16	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩ \leftrightarrow L = ⟨0, (y - 1) \mod 5⟩)$
18	11 13 17	3orbi123d	$⊢ 2^{nd} (X) = y \to ((L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \leftrightarrow (L = ⟨0, (y + 1) \mod 5⟩ \lor L = ⟨1, y⟩ \lor L = ⟨0, (y - 1) \mod 5⟩))$
19	10	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \leftrightarrow K = ⟨0, (y + 1) \mod 5⟩)$
20	12	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨1, 2^{nd} (X)⟩ \leftrightarrow K = ⟨1, y⟩)$
21	16	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩ \leftrightarrow K = ⟨0, (y - 1) \mod 5⟩)$
22	19 20 21	3orbi123d	$⊢ 2^{nd} (X) = y \to ((K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \leftrightarrow (K = ⟨0, (y + 1) \mod 5⟩ \lor K = ⟨1, y⟩ \lor K = ⟨0, (y - 1) \mod 5⟩))$
23	18 22	anbi12d	$⊢ 2^{nd} (X) = y \to (((L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \land (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩)) \leftrightarrow ((L = ⟨0, (y + 1) \mod 5⟩ \lor L = ⟨1, y⟩ \lor L = ⟨0, (y - 1) \mod 5⟩) \land (K = ⟨0, (y + 1) \mod 5⟩ \lor K = ⟨1, y⟩ \lor K = ⟨0, (y - 1) \mod 5⟩)))$
24		simpr	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to K = ⟨0, (y + 1) \mod 5⟩$
25		simpl	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to L = ⟨0, (y + 1) \mod 5⟩$
26	24 25	neeq12d	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to (K \neq L \leftrightarrow ⟨0, (y + 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩)$
27		eqid	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨0, (y + 1) \mod 5⟩$
28		eqneqall	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨0, (y + 1) \mod 5⟩ \to (⟨0, (y + 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
29	27 28	ax-mp	$⊢ ⟨0, (y + 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
30	26 29	biimtrdi	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
31	30	impd	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
32	31	ex	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to (K = ⟨0, (y + 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
33		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
34		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
35		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
36		eqid	$⊢ (0 ..^5) = (0 ..^5)$
37	35 36 1 3	gpgedgiov	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨0, b⟩, ⟨1, y⟩\} \in E \leftrightarrow b = y)$
38	33 34 37	mpanl12	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨0, b⟩, ⟨1, y⟩\} \in E \leftrightarrow b = y)$
39		opeq2	$⊢ y = b \to ⟨0, y⟩ = ⟨0, b⟩$
40	39	eqcoms	$⊢ b = y \to ⟨0, y⟩ = ⟨0, b⟩$
41	38 40	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨0, b⟩, ⟨1, y⟩\} \in E \to ⟨0, y⟩ = ⟨0, b⟩)$
42	41	adantld	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨1, y⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
43		preq1	$⊢ K = ⟨0, (y + 1) \mod 5⟩ \to \{K, ⟨0, b⟩\} = \{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\}$
44	43	eleq1d	$⊢ K = ⟨0, (y + 1) \mod 5⟩ \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E)$
45		preq2	$⊢ L = ⟨1, y⟩ \to \{⟨0, b⟩, L\} = \{⟨0, b⟩, ⟨1, y⟩\}$
46	45	eleq1d	$⊢ L = ⟨1, y⟩ \to (\{⟨0, b⟩, L\} \in E \leftrightarrow \{⟨0, b⟩, ⟨1, y⟩\} \in E)$
47	44 46	bi2anan9r	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨1, y⟩\} \in E))$
48	47	imbi1d	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to (((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩) \leftrightarrow ((\{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨1, y⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
49	42 48	imbitrrid	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
50	49	adantld	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
51	50	ex	$⊢ L = ⟨1, y⟩ \to (K = ⟨0, (y + 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
52		prcom	$⊢ \{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} = \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\}$
53	52	eleq1i	$⊢ \{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
54		prcom	$⊢ \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} = \{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\}$
55	54	eleq1i	$⊢ \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E \leftrightarrow \{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E$
56	53 55	anbi12ci	$⊢ (\{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \leftrightarrow (\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
57		5nn	$⊢ 5 \in ℕ$
58	57	nnzi	$⊢ 5 \in ℤ$
59		uzid	$⊢ 5 \in ℤ \to 5 \in ℤ_{\geq 5}$
60	58 59	ax-mp	$⊢ 5 \in ℤ_{\geq 5}$
61	35 36 1 3	gpgedg2ov	$⊢ ((5 \in ℤ_{\geq 5} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \leftrightarrow b = y)$
62	60 34 61	mpanl12	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \leftrightarrow b = y)$
63		equcomiv	$⊢ b = y \to y = b$
64	63	opeq2d	$⊢ b = y \to ⟨0, y⟩ = ⟨0, b⟩$
65	62 64	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
66	56 65	biimtrid	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
67		preq2	$⊢ L = ⟨0, (y - 1) \mod 5⟩ \to \{⟨0, b⟩, L\} = \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\}$
68	67	eleq1d	$⊢ L = ⟨0, (y - 1) \mod 5⟩ \to (\{⟨0, b⟩, L\} \in E \leftrightarrow \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
69	44 68	bi2anan9r	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E))$
70	69	imbi1d	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to (((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩) \leftrightarrow ((\{⟨0, (y + 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
71	66 70	imbitrrid	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
72	71	adantld	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨0, (y + 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
73	72	ex	$⊢ L = ⟨0, (y - 1) \mod 5⟩ \to (K = ⟨0, (y + 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
74	32 51 73	3jaoi	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \lor L = ⟨1, y⟩ \lor L = ⟨0, (y - 1) \mod 5⟩) \to (K = ⟨0, (y + 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
75		prcom	$⊢ \{⟨1, y⟩, ⟨0, b⟩\} = \{⟨0, b⟩, ⟨1, y⟩\}$
76	75	eleq1i	$⊢ \{⟨1, y⟩, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, b⟩, ⟨1, y⟩\} \in E$
77	76 41	biimtrid	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, y⟩, ⟨0, b⟩\} \in E \to ⟨0, y⟩ = ⟨0, b⟩)$
78	77	adantrd	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, y⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
79		preq1	$⊢ K = ⟨1, y⟩ \to \{K, ⟨0, b⟩\} = \{⟨1, y⟩, ⟨0, b⟩\}$
80	79	eleq1d	$⊢ K = ⟨1, y⟩ \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨1, y⟩, ⟨0, b⟩\} \in E)$
81		preq2	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to \{⟨0, b⟩, L\} = \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\}$
82	81	eleq1d	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to (\{⟨0, b⟩, L\} \in E \leftrightarrow \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
83	80 82	bi2anan9r	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨1, y⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E))$
84	83	imbi1d	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to (((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩) \leftrightarrow ((\{⟨1, y⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
85	78 84	imbitrrid	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
86	85	adantld	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
87	86	ex	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to (K = ⟨1, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
88		simpr	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to K = ⟨1, y⟩$
89		simpl	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to L = ⟨1, y⟩$
90	88 89	neeq12d	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to (K \neq L \leftrightarrow ⟨1, y⟩ \neq ⟨1, y⟩)$
91		eqid	$⊢ ⟨1, y⟩ = ⟨1, y⟩$
92		eqneqall	$⊢ ⟨1, y⟩ = ⟨1, y⟩ \to (⟨1, y⟩ \neq ⟨1, y⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
93	91 92	ax-mp	$⊢ ⟨1, y⟩ \neq ⟨1, y⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
94	90 93	biimtrdi	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
95	94	impd	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
96	95	ex	$⊢ L = ⟨1, y⟩ \to (K = ⟨1, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
97	77	adantrd	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, y⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
98	79	adantl	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to \{K, ⟨0, b⟩\} = \{⟨1, y⟩, ⟨0, b⟩\}$
99	98	eleq1d	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨1, y⟩, ⟨0, b⟩\} \in E)$
100	67	adantr	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to \{⟨0, b⟩, L\} = \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\}$
101	100	eleq1d	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to (\{⟨0, b⟩, L\} \in E \leftrightarrow \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
102	99 101	anbi12d	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨1, y⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E))$
103	102	imbi1d	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to (((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩) \leftrightarrow ((\{⟨1, y⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
104	97 103	imbitrrid	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
105	104	adantld	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
106	105	ex	$⊢ L = ⟨0, (y - 1) \mod 5⟩ \to (K = ⟨1, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
107	87 96 106	3jaoi	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \lor L = ⟨1, y⟩ \lor L = ⟨0, (y - 1) \mod 5⟩) \to (K = ⟨1, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
108	62 40	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
109	108	adantl	$⊢ (⟨0, (y - 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩ \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
110	109	a1i	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to ((⟨0, (y - 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩ \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
111		simpl	$⊢ (K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨0, (y + 1) \mod 5⟩) \to K = ⟨0, (y - 1) \mod 5⟩$
112		simpr	$⊢ (K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨0, (y + 1) \mod 5⟩) \to L = ⟨0, (y + 1) \mod 5⟩$
113	111 112	neeq12d	$⊢ (K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨0, (y + 1) \mod 5⟩) \to (K \neq L \leftrightarrow ⟨0, (y - 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩)$
114	113	ancoms	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to (K \neq L \leftrightarrow ⟨0, (y - 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩)$
115	114	anbi1d	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \leftrightarrow (⟨0, (y - 1) \mod 5⟩ \neq ⟨0, (y + 1) \mod 5⟩ \land (b \in (0 ..^5) \land y \in (0 ..^5))))$
116		preq1	$⊢ K = ⟨0, (y - 1) \mod 5⟩ \to \{K, ⟨0, b⟩\} = \{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\}$
117	116	eleq1d	$⊢ K = ⟨0, (y - 1) \mod 5⟩ \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E)$
118	117 82	bi2anan9r	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E))$
119	118	imbi1d	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to (((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩) \leftrightarrow ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
120	110 115 119	3imtr4d	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
121	120	ex	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to (K = ⟨0, (y - 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
122	41	adantld	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨1, y⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
123	122	adantl	$⊢ (K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨1, y⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)$
124	116	adantl	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to \{K, ⟨0, b⟩\} = \{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\}$
125	124	eleq1d	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E)$
126	46	adantr	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to (\{⟨0, b⟩, L\} \in E \leftrightarrow \{⟨0, b⟩, ⟨1, y⟩\} \in E)$
127	125 126	anbi12d	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨1, y⟩\} \in E))$
128	127	imbi1d	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to (((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩) \leftrightarrow ((\{⟨0, (y - 1) \mod 5⟩, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, ⟨1, y⟩\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
129	123 128	imbitrrid	$⊢ (L = ⟨1, y⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
130	129	ex	$⊢ L = ⟨1, y⟩ \to (K = ⟨0, (y - 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
131		eqeq2	$⊢ ⟨0, (y - 1) \mod 5⟩ = L \to (K = ⟨0, (y - 1) \mod 5⟩ \leftrightarrow K = L)$
132	131	eqcoms	$⊢ L = ⟨0, (y - 1) \mod 5⟩ \to (K = ⟨0, (y - 1) \mod 5⟩ \leftrightarrow K = L)$
133		eqneqall	$⊢ K = L \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
134	133	impd	$⊢ K = L \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
135	132 134	biimtrdi	$⊢ L = ⟨0, (y - 1) \mod 5⟩ \to (K = ⟨0, (y - 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
136	121 130 135	3jaoi	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \lor L = ⟨1, y⟩ \lor L = ⟨0, (y - 1) \mod 5⟩) \to (K = ⟨0, (y - 1) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
137	74 107 136	3jaod	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \lor L = ⟨1, y⟩ \lor L = ⟨0, (y - 1) \mod 5⟩) \to ((K = ⟨0, (y + 1) \mod 5⟩ \lor K = ⟨1, y⟩ \lor K = ⟨0, (y - 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
138	137	imp	$⊢ ((L = ⟨0, (y + 1) \mod 5⟩ \lor L = ⟨1, y⟩ \lor L = ⟨0, (y - 1) \mod 5⟩) \land (K = ⟨0, (y + 1) \mod 5⟩ \lor K = ⟨1, y⟩ \lor K = ⟨0, (y - 1) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
139	23 138	biimtrdi	$⊢ 2^{nd} (X) = y \to (((L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \land (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
140	7 139	syl	$⊢ X = ⟨0, y⟩ \to (((L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \land (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
141		eqeq1	$⊢ X = ⟨0, y⟩ \to (X = ⟨0, b⟩ \leftrightarrow ⟨0, y⟩ = ⟨0, b⟩)$
142	141	imbi2d	$⊢ X = ⟨0, y⟩ \to (((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩) \leftrightarrow ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩))$
143	142	imbi2d	$⊢ X = ⟨0, y⟩ \to (((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)) \leftrightarrow ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to ⟨0, y⟩ = ⟨0, b⟩)))$
144	140 143	sylibrd	$⊢ X = ⟨0, y⟩ \to (((L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \land (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
145	144	adantl	$⊢ (X \in V \land X = ⟨0, y⟩) \to (((L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \land (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
146	145	expdcom	$⊢ (L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \to ((K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \to ((X \in V \land X = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$

Metamath Proof Explorer

Theorem pgnbgreunbgrlem1

Proof