pgnbgreunbgrlem2

Description: Lemma 2 for pgnbgreunbgr . Impossible cases. (Contributed by AV, 18-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	pgnbgreunbgrlem2	$⊢ (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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		eqtr3	$⊢ (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩) \to L = K$
6		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 X = ⟨0, b⟩)))$
7	6	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 X = ⟨0, b⟩))$
8	7	eqcoms	$⊢ L = K \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⟩))$
9	5 8	syl	$⊢ (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) + 2) \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⟩))$
10	9	a1d	$⊢ (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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⟩)))$
11	10	ex	$⊢ L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \to (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
12		1ex	$⊢ 1 \in V$
13		vex	$⊢ y \in V$
14	12 13	op2ndd	$⊢ X = ⟨1, y⟩ \to 2^{nd} (X) = y$
15		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) + 2 = y + 2$
16	15	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) + 2) \mod 5 = (y + 2) \mod 5$
17	16	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) + 2) \mod 5⟩ = ⟨1, (y + 2) \mod 5⟩$
18	17	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \leftrightarrow L = ⟨1, (y + 2) \mod 5⟩)$
19		opeq2	$⊢ 2^{nd} (X) = y \to ⟨0, 2^{nd} (X)⟩ = ⟨0, y⟩$
20	19	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨0, 2^{nd} (X)⟩ \leftrightarrow K = ⟨0, y⟩)$
21	18 20	anbi12d	$⊢ 2^{nd} (X) = y \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨0, 2^{nd} (X)⟩) \leftrightarrow (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩))$
22	14 21	syl	$⊢ X = ⟨1, y⟩ \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨0, 2^{nd} (X)⟩) \leftrightarrow (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩))$
23	1 2 3 4	pgnbgreunbgrlem2lem1	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, L\} \in E$
24	23	pm2.21d	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to (\{⟨0, b⟩, L\} \in E \to X = ⟨0, b⟩)$
25	24	expimpd	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \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⟩)$
26	25	ex	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((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⟩))$
27	26	adantld	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨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⟩))$
28	22 27	biimtrdi	$⊢ X = ⟨1, y⟩ \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨0, 2^{nd} (X)⟩) \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⟩)))$
29	28	adantr	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨0, 2^{nd} (X)⟩) \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⟩)))$
30	29	expdcom	$⊢ L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \to (K = ⟨0, 2^{nd} (X)⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
31		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) - 2 = y - 2$
32	31	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) - 2) \mod 5 = (y - 2) \mod 5$
33	32	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) - 2) \mod 5⟩ = ⟨1, (y - 2) \mod 5⟩$
34	33	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \leftrightarrow K = ⟨1, (y - 2) \mod 5⟩)$
35	18 34	anbi12d	$⊢ 2^{nd} (X) = y \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \leftrightarrow (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩))$
36	14 35	syl	$⊢ X = ⟨1, y⟩ \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \leftrightarrow (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩))$
37	1 2 3 4	pgnbgreunbgrlem2lem3	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, L\} \in E$
38	37	pm2.21d	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to (\{⟨0, b⟩, L\} \in E \to X = ⟨0, b⟩)$
39	38	expimpd	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \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⟩)$
40	39	ex	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \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 X = ⟨0, b⟩))$
41	40	adantld	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \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⟩))$
42	36 41	biimtrdi	$⊢ X = ⟨1, y⟩ \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \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⟩)))$
43	42	adantr	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \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⟩)))$
44	43	expdcom	$⊢ L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \to (K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
45	11 30 44	3jaod	$⊢ L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
46	14	adantr	$⊢ (X = ⟨1, y⟩ \land X \in V) \to 2^{nd} (X) = y$
47	19	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨0, 2^{nd} (X)⟩ \leftrightarrow L = ⟨0, y⟩)$
48	17	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \leftrightarrow K = ⟨1, (y + 2) \mod 5⟩)$
49	47 48	anbi12d	$⊢ 2^{nd} (X) = y \to ((L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩) \leftrightarrow (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \mod 5⟩))$
50	46 49	syl	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩) \leftrightarrow (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \mod 5⟩))$
51		prcom	$⊢ \{⟨0, b⟩, L\} = \{L, ⟨0, b⟩\}$
52	51	eleq1i	$⊢ \{⟨0, b⟩, L\} \in E \leftrightarrow \{L, ⟨0, b⟩\} \in E$
53	1 2 3 4	pgnbgreunbgrlem2lem1	$⊢ (((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, K\} \in E$
54		prcom	$⊢ \{K, ⟨0, b⟩\} = \{⟨0, b⟩, K\}$
55	54	eleq1i	$⊢ \{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, b⟩, K\} \in E$
56		pm2.21	$⊢ \neg \{⟨0, b⟩, K\} \in E \to (\{⟨0, b⟩, K\} \in E \to X = ⟨0, b⟩)$
57	55 56	biimtrid	$⊢ \neg \{⟨0, b⟩, K\} \in E \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩)$
58	53 57	syl	$⊢ (((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨0, b⟩\} \in E) \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩)$
59	58	ex	$⊢ ((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{L, ⟨0, b⟩\} \in E \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩))$
60	52 59	biimtrid	$⊢ ((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨0, b⟩, L\} \in E \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩))$
61	60	impcomd	$⊢ ((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨0, y⟩) \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⟩)$
62	61	ex	$⊢ (K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨0, y⟩) \to ((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⟩))$
63	62	ancoms	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \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 X = ⟨0, b⟩))$
64	63	adantld	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \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⟩))$
65	50 64	biimtrdi	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨1, (2^{nd} (X) + 2) \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⟩)))$
66	65	expdcom	$⊢ L = ⟨0, 2^{nd} (X)⟩ \to (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
67		eqtr3	$⊢ (K = ⟨0, 2^{nd} (X)⟩ \land L = ⟨0, 2^{nd} (X)⟩) \to K = L$
68	67	ancoms	$⊢ (L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨0, 2^{nd} (X)⟩) \to K = L$
69	68 6	syl	$⊢ (L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨0, 2^{nd} (X)⟩) \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 X = ⟨0, b⟩)))$
70	69	impd	$⊢ (L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨0, 2^{nd} (X)⟩) \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⟩))$
71	70	a1d	$⊢ (L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨0, 2^{nd} (X)⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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⟩)))$
72	71	ex	$⊢ L = ⟨0, 2^{nd} (X)⟩ \to (K = ⟨0, 2^{nd} (X)⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
73	47 34	anbi12d	$⊢ 2^{nd} (X) = y \to ((L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \leftrightarrow (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩))$
74	46 73	syl	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \leftrightarrow (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩))$
75	1 2 3 4	pgnbgreunbgrlem2lem2	$⊢ (((K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, K\} \in E$
76	75 57	syl	$⊢ (((K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨0, b⟩\} \in E) \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩)$
77	76	ex	$⊢ ((K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{L, ⟨0, b⟩\} \in E \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩))$
78	52 77	biimtrid	$⊢ ((K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨0, b⟩, L\} \in E \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩))$
79	78	impcomd	$⊢ ((K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨0, y⟩) \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⟩)$
80	79	ex	$⊢ (K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨0, y⟩) \to ((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⟩))$
81	80	ancoms	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \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 X = ⟨0, b⟩))$
82	81	adantld	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \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⟩))$
83	74 82	biimtrdi	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨0, 2^{nd} (X)⟩ \land K = ⟨1, (2^{nd} (X) - 2) \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⟩)))$
84	83	expdcom	$⊢ L = ⟨0, 2^{nd} (X)⟩ \to (K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
85	66 72 84	3jaod	$⊢ L = ⟨0, 2^{nd} (X)⟩ \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
86	33	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \leftrightarrow L = ⟨1, (y - 2) \mod 5⟩)$
87	86 48	anbi12d	$⊢ 2^{nd} (X) = y \to ((L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩) \leftrightarrow (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩))$
88	46 87	syl	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩) \leftrightarrow (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩))$
89	1 2 3 4	pgnbgreunbgrlem2lem3	$⊢ (((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, K\} \in E$
90	89 57	syl	$⊢ (((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{L, ⟨0, b⟩\} \in E) \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩)$
91	90	ex	$⊢ ((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{L, ⟨0, b⟩\} \in E \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩))$
92	52 91	biimtrid	$⊢ ((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨0, b⟩, L\} \in E \to (\{K, ⟨0, b⟩\} \in E \to X = ⟨0, b⟩))$
93	92	impcomd	$⊢ ((K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨1, (y - 2) \mod 5⟩) \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⟩)$
94	93	ex	$⊢ (K = ⟨1, (y + 2) \mod 5⟩ \land L = ⟨1, (y - 2) \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 X = ⟨0, b⟩))$
95	94	ancoms	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \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 X = ⟨0, b⟩))$
96	95	adantld	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \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⟩))$
97	88 96	biimtrdi	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) + 2) \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⟩)))$
98	97	expdcom	$⊢ L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \to (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
99	86 20	anbi12d	$⊢ 2^{nd} (X) = y \to ((L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨0, 2^{nd} (X)⟩) \leftrightarrow (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩))$
100	46 99	syl	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨0, 2^{nd} (X)⟩) \leftrightarrow (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩))$
101	1 2 3 4	pgnbgreunbgrlem2lem2	$⊢ (((L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, L\} \in E$
102	101	pm2.21d	$⊢ (((L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to (\{⟨0, b⟩, L\} \in E \to X = ⟨0, b⟩)$
103	102	expimpd	$⊢ ((L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \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⟩)$
104	103	ex	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((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⟩))$
105	104	adantld	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨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⟩))$
106	100 105	biimtrdi	$⊢ (X = ⟨1, y⟩ \land X \in V) \to ((L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨0, 2^{nd} (X)⟩) \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⟩)))$
107	106	expdcom	$⊢ L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \to (K = ⟨0, 2^{nd} (X)⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
108		eqtr3	$⊢ (L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to L = K$
109	108	eqcomd	$⊢ (L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to K = L$
110	109 7	syl	$⊢ (L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \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⟩))$
111	110	a1d	$⊢ (L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \land K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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⟩)))$
112	111	ex	$⊢ L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \to (K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
113	98 107 112	3jaod	$⊢ L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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⟩))))$
114	45 85 113	3jaoi	$⊢ (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X = ⟨1, y⟩ \land X \in V) \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 pgnbgreunbgrlem2

Proof