pgnbgreunbgrlem5lem3

Description: Lemma 3 for pgnbgreunbgrlem5 . (Contributed by AV, 20-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	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$

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

Metamath Proof Explorer

Theorem pgnbgreunbgrlem5lem3

Proof