pgnbgreunbgrlem5

Description: Lemma 5 for pgnbgreunbgr . Impossible cases. (Contributed by AV, 21-Nov-2025)

	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	pgnbgreunbgrlem5	$⊢ (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 = ⟨0, y⟩ \land X \in V) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, 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	7	adantr	$⊢ (X = ⟨0, y⟩ \land X \in V) \to 2^{nd} (X) = y$
9		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) + 1 = y + 1$
10	9	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) + 1) \mod 5 = (y + 1) \mod 5$
11	10	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨0, (2^{nd} (X) + 1) \mod 5⟩ = ⟨0, (y + 1) \mod 5⟩$
12	11	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \leftrightarrow L = ⟨0, (y + 1) \mod 5⟩)$
13		opeq2	$⊢ 2^{nd} (X) = y \to ⟨1, 2^{nd} (X)⟩ = ⟨1, y⟩$
14	13	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨1, 2^{nd} (X)⟩ \leftrightarrow L = ⟨1, y⟩)$
15		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) - 1 = y - 1$
16	15	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) - 1) \mod 5 = (y - 1) \mod 5$
17	16	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨0, (2^{nd} (X) - 1) \mod 5⟩ = ⟨0, (y - 1) \mod 5⟩$
18	17	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩ \leftrightarrow L = ⟨0, (y - 1) \mod 5⟩)$
19	12 14 18	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⟩))$
20	11	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \leftrightarrow K = ⟨0, (y + 1) \mod 5⟩)$
21	13	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨1, 2^{nd} (X)⟩ \leftrightarrow K = ⟨1, y⟩)$
22	17	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩ \leftrightarrow K = ⟨0, (y - 1) \mod 5⟩)$
23	20 21 22	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⟩))$
24	19 23	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⟩)))$
25	8 24	syl	$⊢ (X = ⟨0, y⟩ \land X \in V) \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⟩)))$
26		simpl	$⊢ (K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y + 1) \mod 5⟩) \to K = ⟨0, (y + 1) \mod 5⟩$
27		simpr	$⊢ (K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y + 1) \mod 5⟩) \to L = ⟨0, (y + 1) \mod 5⟩$
28	26 27	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⟩)$
29	28	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⟩)$
30		eqid	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨0, (y + 1) \mod 5⟩$
31		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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
32	30 31	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
33	29 32	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
34	33	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
35	34	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
36	1 2 3 4	pgnbgreunbgrlem5lem1	$⊢ (((L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨1, b⟩\} \in E) \to \neg \{⟨1, b⟩, L\} \in E$
37	36	pm2.21d	$⊢ (((L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨1, b⟩\} \in E) \to (\{⟨1, b⟩, L\} \in E \to X = ⟨1, b⟩)$
38	37	expimpd	$⊢ ((L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
39	38	ex	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
40	39	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
41	40	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
42	1 2 3 4	pgnbgreunbgrlem5lem3	$⊢ (((L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨1, b⟩\} \in E) \to \neg \{⟨1, b⟩, L\} \in E$
43	42	pm2.21d	$⊢ (((L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨1, b⟩\} \in E) \to (\{⟨1, b⟩, L\} \in E \to X = ⟨1, b⟩)$
44	43	expimpd	$⊢ ((L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
45	44	ex	$⊢ (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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
46	45	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
47	46	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
48	35 41 47	3jaod	$⊢ 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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
49		prcom	$⊢ \{K, ⟨1, b⟩\} = \{⟨1, b⟩, K\}$
50	49	eleq1i	$⊢ \{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨1, b⟩, K\} \in E$
51		prcom	$⊢ \{⟨1, b⟩, L\} = \{L, ⟨1, b⟩\}$
52	51	eleq1i	$⊢ \{⟨1, b⟩, L\} \in E \leftrightarrow \{L, ⟨1, b⟩\} \in E$
53	50 52	anbi12i	$⊢ (\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨1, b⟩, K\} \in E \land \{L, ⟨1, b⟩\} \in E)$
54	1 2 3 4	pgnbgreunbgrlem5lem1	$⊢ (((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨1, b⟩\} \in E) \to \neg \{⟨1, b⟩, K\} \in E$
55	54	pm2.21d	$⊢ (((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨1, b⟩\} \in E) \to (\{⟨1, b⟩, K\} \in E \to X = ⟨1, b⟩)$
56	55	ex	$⊢ ((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{L, ⟨1, b⟩\} \in E \to (\{⟨1, b⟩, K\} \in E \to X = ⟨1, b⟩))$
57	56	impcomd	$⊢ ((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨1, b⟩, K\} \in E \land \{L, ⟨1, b⟩\} \in E) \to X = ⟨1, b⟩)$
58	53 57	biimtrid	$⊢ ((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
59	58	ex	$⊢ (K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨1, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
60	59	adantld	$⊢ (K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
61	60	expcom	$⊢ 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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
62		simpr	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to K = ⟨1, y⟩$
63		simpl	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to L = ⟨1, y⟩$
64	62 63	neeq12d	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to (K \neq L \leftrightarrow ⟨1, y⟩ \neq ⟨1, y⟩)$
65		eqid	$⊢ ⟨1, y⟩ = ⟨1, y⟩$
66		eqneqall	$⊢ ⟨1, y⟩ = ⟨1, y⟩ \to (⟨1, y⟩ \neq ⟨1, y⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
67	65 66	ax-mp	$⊢ ⟨1, y⟩ \neq ⟨1, y⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
68	64 67	biimtrdi	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
69	68	impd	$⊢ (L = ⟨1, y⟩ \land K = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
70	69	ex	$⊢ L = ⟨1, y⟩ \to (K = ⟨1, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
71	1 2 3 4	pgnbgreunbgrlem5lem2	$⊢ (((K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨1, b⟩\} \in E) \to \neg \{⟨1, b⟩, K\} \in E$
72	71	pm2.21d	$⊢ (((K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨1, b⟩\} \in E) \to (\{⟨1, b⟩, K\} \in E \to X = ⟨1, b⟩)$
73	72	ex	$⊢ ((K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{L, ⟨1, b⟩\} \in E \to (\{⟨1, b⟩, K\} \in E \to X = ⟨1, b⟩))$
74	73	impcomd	$⊢ ((K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨1, b⟩, K\} \in E \land \{L, ⟨1, b⟩\} \in E) \to X = ⟨1, b⟩)$
75	53 74	biimtrid	$⊢ ((K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
76	75	ex	$⊢ (K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨1, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
77	76	adantld	$⊢ (K = ⟨0, (y - 1) \mod 5⟩ \land L = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
78	77	expcom	$⊢ 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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
79	61 70 78	3jaod	$⊢ L = ⟨1, y⟩ \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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
80	1 2 3 4	pgnbgreunbgrlem5lem3	$⊢ (((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨1, b⟩\} \in E) \to \neg \{⟨1, b⟩, K\} \in E$
81	80	pm2.21d	$⊢ (((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨1, b⟩\} \in E) \to (\{⟨1, b⟩, K\} \in E \to X = ⟨1, b⟩)$
82	81	ex	$⊢ ((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{L, ⟨1, b⟩\} \in E \to (\{⟨1, b⟩, K\} \in E \to X = ⟨1, b⟩))$
83	82	impcomd	$⊢ ((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨1, b⟩, K\} \in E \land \{L, ⟨1, b⟩\} \in E) \to X = ⟨1, b⟩)$
84	53 83	biimtrid	$⊢ ((K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y - 1) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
85	84	ex	$⊢ (K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y - 1) \mod 5⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
86	85	adantld	$⊢ (K = ⟨0, (y + 1) \mod 5⟩ \land L = ⟨0, (y - 1) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
87	86	expcom	$⊢ 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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
88	1 2 3 4	pgnbgreunbgrlem5lem2	$⊢ (((L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨1, b⟩\} \in E) \to \neg \{⟨1, b⟩, L\} \in E$
89	88	pm2.21d	$⊢ (((L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨1, b⟩\} \in E) \to (\{⟨1, b⟩, L\} \in E \to X = ⟨1, b⟩)$
90	89	expimpd	$⊢ ((L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
91	90	ex	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
92	91	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
93	92	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
94		simpr	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to K = ⟨0, (y - 1) \mod 5⟩$
95		simpl	$⊢ (L = ⟨0, (y - 1) \mod 5⟩ \land K = ⟨0, (y - 1) \mod 5⟩) \to L = ⟨0, (y - 1) \mod 5⟩$
96	94 95	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⟩)$
97		eqid	$⊢ ⟨0, (y - 1) \mod 5⟩ = ⟨0, (y - 1) \mod 5⟩$
98		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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
99	97 98	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
100	96 99	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
101	100	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
102	101	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
103	87 93 102	3jaod	$⊢ 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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
104	48 79 103	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⟩ \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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
105	104	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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
106	25 105	biimtrdi	$⊢ (X = ⟨0, y⟩ \land X \in V) \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, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
107	106	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 = ⟨0, y⟩ \land X \in V) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$

Metamath Proof Explorer

Theorem pgnbgreunbgrlem5

Proof