pgnbgreunbgrlem5lem1

Description: Lemma 1 for pgnbgreunbgrlem5 . (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	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$

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		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
6		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
7	5 6	pm3.2i	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉))$
8		1ex	$⊢ 1 \in V$
9		vex	$⊢ y \in V$
10	8 9	op1st	$⊢ 1^{st} (⟨1, y⟩) = 1$
11		simpr	$⊢ ((b \in (0 ..^5) \land y \in (0 ..^5)) \land \{⟨1, y⟩, ⟨1, b⟩\} \in E) \to \{⟨1, y⟩, ⟨1, b⟩\} \in E$
12		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
13	12 1 2 3	gpgvtxedg1	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land 1^{st} (⟨1, y⟩) = 1 \land \{⟨1, y⟩, ⟨1, b⟩\} \in E) \to (⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) + 2) \mod 5⟩ \lor ⟨1, b⟩ = ⟨0, 2^{nd} (⟨1, y⟩)⟩ \lor ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) - 2) \mod 5⟩)$
14	7 10 11 13	mp3an12i	$⊢ ((b \in (0 ..^5) \land y \in (0 ..^5)) \land \{⟨1, y⟩, ⟨1, b⟩\} \in E) \to (⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) + 2) \mod 5⟩ \lor ⟨1, b⟩ = ⟨0, 2^{nd} (⟨1, y⟩)⟩ \lor ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) - 2) \mod 5⟩)$
15	14	ex	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, y⟩, ⟨1, b⟩\} \in E \to (⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) + 2) \mod 5⟩ \lor ⟨1, b⟩ = ⟨0, 2^{nd} (⟨1, y⟩)⟩ \lor ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) - 2) \mod 5⟩))$
16		vex	$⊢ b \in V$
17	8 16	opth	$⊢ ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) + 2) \mod 5⟩ \leftrightarrow (1 = 1 \land b = (2^{nd} (⟨1, y⟩) + 2) \mod 5)$
18	8 9	op2nd	$⊢ 2^{nd} (⟨1, y⟩) = y$
19	18	oveq1i	$⊢ 2^{nd} (⟨1, y⟩) + 2 = y + 2$
20	19	oveq1i	$⊢ (2^{nd} (⟨1, y⟩) + 2) \mod 5 = (y + 2) \mod 5$
21	20	eqeq2i	$⊢ b = (2^{nd} (⟨1, y⟩) + 2) \mod 5 \leftrightarrow b = (y + 2) \mod 5$
22	1 3	pgnioedg2	$⊢ y \in (0 ..^5) \to \neg \{⟨1, (y + 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
23	22	adantl	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, (y + 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
24		opeq2	$⊢ b = (y + 2) \mod 5 \to ⟨1, b⟩ = ⟨1, (y + 2) \mod 5⟩$
25	24	preq1d	$⊢ b = (y + 2) \mod 5 \to \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} = \{⟨1, (y + 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\}$
26	25	eleq1d	$⊢ b = (y + 2) \mod 5 \to (\{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E \leftrightarrow \{⟨1, (y + 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
27	26	notbid	$⊢ b = (y + 2) \mod 5 \to (\neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E \leftrightarrow \neg \{⟨1, (y + 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
28	23 27	imbitrrid	$⊢ b = (y + 2) \mod 5 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
29	21 28	sylbi	$⊢ b = (2^{nd} (⟨1, y⟩) + 2) \mod 5 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
30	17 29	simplbiim	$⊢ ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) + 2) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
31	30	com12	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) + 2) \mod 5⟩ \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
32	8 16	opth	$⊢ ⟨1, b⟩ = ⟨0, 2^{nd} (⟨1, y⟩)⟩ \leftrightarrow (1 = 0 \land b = 2^{nd} (⟨1, y⟩))$
33		ax-1ne0	$⊢ 1 \neq 0$
34		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
35	33 34	mpi	$⊢ 1 = 0 \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
36	35	adantr	$⊢ (1 = 0 \land b = 2^{nd} (⟨1, y⟩)) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
37	32 36	sylbi	$⊢ ⟨1, b⟩ = ⟨0, 2^{nd} (⟨1, y⟩)⟩ \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
38	37	a1i	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (⟨1, b⟩ = ⟨0, 2^{nd} (⟨1, y⟩)⟩ \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
39	8 16	opth	$⊢ ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) - 2) \mod 5⟩ \leftrightarrow (1 = 1 \land b = (2^{nd} (⟨1, y⟩) - 2) \mod 5)$
40	18	oveq1i	$⊢ 2^{nd} (⟨1, y⟩) - 2 = y - 2$
41	40	oveq1i	$⊢ (2^{nd} (⟨1, y⟩) - 2) \mod 5 = (y - 2) \mod 5$
42	41	eqeq2i	$⊢ b = (2^{nd} (⟨1, y⟩) - 2) \mod 5 \leftrightarrow b = (y - 2) \mod 5$
43	1 3	pgnioedg1	$⊢ y \in (0 ..^5) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
44	43	adantl	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
45		opeq2	$⊢ b = (y - 2) \mod 5 \to ⟨1, b⟩ = ⟨1, (y - 2) \mod 5⟩$
46	45	preq1d	$⊢ b = (y - 2) \mod 5 \to \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} = \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\}$
47	46	eleq1d	$⊢ b = (y - 2) \mod 5 \to (\{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E \leftrightarrow \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
48	47	notbid	$⊢ b = (y - 2) \mod 5 \to (\neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E \leftrightarrow \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
49	44 48	imbitrrid	$⊢ b = (y - 2) \mod 5 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
50	42 49	sylbi	$⊢ b = (2^{nd} (⟨1, y⟩) - 2) \mod 5 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
51	39 50	simplbiim	$⊢ ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) - 2) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
52	51	com12	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) - 2) \mod 5⟩ \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
53	31 38 52	3jaod	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) + 2) \mod 5⟩ \lor ⟨1, b⟩ = ⟨0, 2^{nd} (⟨1, y⟩)⟩ \lor ⟨1, b⟩ = ⟨1, (2^{nd} (⟨1, y⟩) - 2) \mod 5⟩) \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
54	15 53	syld	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, y⟩, ⟨1, b⟩\} \in E \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
55	54	adantl	$⊢ ((L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨1, y⟩, ⟨1, b⟩\} \in E \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
56		preq1	$⊢ K = ⟨1, y⟩ \to \{K, ⟨1, b⟩\} = \{⟨1, y⟩, ⟨1, b⟩\}$
57	56	eleq1d	$⊢ K = ⟨1, y⟩ \to (\{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨1, y⟩, ⟨1, b⟩\} \in E)$
58	57	adantl	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to (\{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨1, y⟩, ⟨1, b⟩\} \in E)$
59		preq2	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to \{⟨1, b⟩, L\} = \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\}$
60	59	eleq1d	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to (\{⟨1, b⟩, L\} \in E \leftrightarrow \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
61	60	notbid	$⊢ L = ⟨0, (y + 1) \mod 5⟩ \to (\neg \{⟨1, b⟩, L\} \in E \leftrightarrow \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
62	61	adantr	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to (\neg \{⟨1, b⟩, L\} \in E \leftrightarrow \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
63	58 62	imbi12d	$⊢ (L = ⟨0, (y + 1) \mod 5⟩ \land K = ⟨1, y⟩) \to ((\{K, ⟨1, b⟩\} \in E \to \neg \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨1, y⟩, ⟨1, b⟩\} \in E \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E))$
64	63	adantr	$⊢ ((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 \to \neg \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨1, y⟩, ⟨1, b⟩\} \in E \to \neg \{⟨1, b⟩, ⟨0, (y + 1) \mod 5⟩\} \in E))$
65	55 64	mpbird	$⊢ ((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 \to \neg \{⟨1, b⟩, L\} \in E)$
66	65	imp	$⊢ (((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$

Metamath Proof Explorer

Theorem pgnbgreunbgrlem5lem1

Proof