pgnioedg5

Description: An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025)

	Ref	Expression
Hypotheses	pgnioedg1.g	No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
	pgnioedg1.e	$⊢ E = Edg (G)$
Assertion	pgnioedg5	$⊢ y \in (0 ..^5) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$

Proof

Step	Hyp	Ref	Expression
1		pgnioedg1.g	Could not format G = ( 5 gPetersenGr 2 ) : No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
2		pgnioedg1.e	$⊢ E = Edg (G)$
3		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
4		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
5	3 4	pm3.2i	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉))$
6		1ex	$⊢ 1 \in V$
7		ovex	$⊢ (y - 1) \mod 5 \in V$
8	6 7	op1st	$⊢ 1^{st} (⟨1, (y - 1) \mod 5⟩) = 1$
9		simpr	$⊢ (y \in (0 ..^5) \land \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
10		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
11		eqid	$⊢ Vtx (G) = Vtx (G)$
12	10 1 11 2	gpgvtxedg1	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land 1^{st} (⟨1, (y - 1) \mod 5⟩) = 1 \land \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to (⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 1) \mod 5⟩)⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5⟩)$
13	5 8 9 12	mp3an12i	$⊢ (y \in (0 ..^5) \land \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E) \to (⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 1) \mod 5⟩)⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5⟩)$
14	13	ex	$⊢ y \in (0 ..^5) \to (\{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E \to (⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 1) \mod 5⟩)⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5⟩))$
15		c0ex	$⊢ 0 \in V$
16		ovex	$⊢ (y + 1) \mod 5 \in V$
17	15 16	opth	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5⟩ \leftrightarrow (0 = 1 \land (y + 1) \mod 5 = (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5)$
18		0ne1	$⊢ 0 \neq 1$
19		eqneqall	$⊢ 0 = 1 \to (0 \neq 1 \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
20	18 19	mpi	$⊢ 0 = 1 \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
21	20	adantr	$⊢ (0 = 1 \land (y + 1) \mod 5 = (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
22	17 21	sylbi	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5⟩ \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
23	22	a1i	$⊢ y \in (0 ..^5) \to (⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5⟩ \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
24	15 16	opth	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 1) \mod 5⟩)⟩ \leftrightarrow (0 = 0 \land (y + 1) \mod 5 = 2^{nd} (⟨1, (y - 1) \mod 5⟩))$
25	6 7	op2nd	$⊢ 2^{nd} (⟨1, (y - 1) \mod 5⟩) = (y - 1) \mod 5$
26	25	eqeq2i	$⊢ (y + 1) \mod 5 = 2^{nd} (⟨1, (y - 1) \mod 5⟩) \leftrightarrow (y + 1) \mod 5 = (y - 1) \mod 5$
27		eqid	$⊢ (0 ..^5) = (0 ..^5)$
28	27	modm1nep1	$⊢ (5 \in ℤ_{\geq 3} \land y \in (0 ..^5)) \to (y - 1) \mod 5 \neq (y + 1) \mod 5$
29	3 28	mpan	$⊢ y \in (0 ..^5) \to (y - 1) \mod 5 \neq (y + 1) \mod 5$
30	29	necomd	$⊢ y \in (0 ..^5) \to (y + 1) \mod 5 \neq (y - 1) \mod 5$
31		eqneqall	$⊢ (y + 1) \mod 5 = (y - 1) \mod 5 \to ((y + 1) \mod 5 \neq (y - 1) \mod 5 \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
32	30 31	syl5	$⊢ (y + 1) \mod 5 = (y - 1) \mod 5 \to (y \in (0 ..^5) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
33	26 32	sylbi	$⊢ (y + 1) \mod 5 = 2^{nd} (⟨1, (y - 1) \mod 5⟩) \to (y \in (0 ..^5) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
34	24 33	simplbiim	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 1) \mod 5⟩)⟩ \to (y \in (0 ..^5) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
35	34	com12	$⊢ y \in (0 ..^5) \to (⟨0, (y + 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 1) \mod 5⟩)⟩ \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
36	15 16	opth	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5⟩ \leftrightarrow (0 = 1 \land (y + 1) \mod 5 = (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5)$
37	20	adantr	$⊢ (0 = 1 \land (y + 1) \mod 5 = (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
38	36 37	sylbi	$⊢ ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5⟩ \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$
39	38	a1i	$⊢ y \in (0 ..^5) \to (⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5⟩ \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
40	23 35 39	3jaod	$⊢ y \in (0 ..^5) \to ((⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 1) \mod 5⟩)⟩ \lor ⟨0, (y + 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 1) \mod 5⟩) - 2) \mod 5⟩) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
41	14 40	syld	$⊢ y \in (0 ..^5) \to (\{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E)$
42	41	pm2.01d	$⊢ y \in (0 ..^5) \to \neg \{⟨1, (y - 1) \mod 5⟩, ⟨0, (y + 1) \mod 5⟩\} \in E$

Metamath Proof Explorer

Theorem pgnioedg5

Proof