pgnioedg4

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	pgnioedg4	$⊢ y \in (0 ..^5) \to \neg \{⟨1, (y - 2) \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 - 2) \mod 5 \in V$
8	6 7	op1st	$⊢ 1^{st} (⟨1, (y - 2) \mod 5⟩) = 1$
9		simpr	$⊢ (y \in (0 ..^5) \land \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \to \{⟨1, (y - 2) \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 - 2) \mod 5⟩) = 1 \land \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \to (⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 2) \mod 5⟩)⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5⟩)$
13	5 8 9 12	mp3an12i	$⊢ (y \in (0 ..^5) \land \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E) \to (⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 2) \mod 5⟩)⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5⟩)$
14	13	ex	$⊢ y \in (0 ..^5) \to (\{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E \to (⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 2) \mod 5⟩)⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \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 - 2) \mod 5⟩) + 2) \mod 5⟩ \leftrightarrow (0 = 1 \land (y - 1) \mod 5 = (2^{nd} (⟨1, (y - 2) \mod 5⟩) + 2) \mod 5)$
18		0ne1	$⊢ 0 \neq 1$
19		eqneqall	$⊢ 0 = 1 \to (0 \neq 1 \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
20	18 19	mpi	$⊢ 0 = 1 \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E$
21	20	adantr	$⊢ (0 = 1 \land (y - 1) \mod 5 = (2^{nd} (⟨1, (y - 2) \mod 5⟩) + 2) \mod 5) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E$
22	17 21	sylbi	$⊢ ⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) + 2) \mod 5⟩ \to \neg \{⟨1, (y - 2) \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 - 2) \mod 5⟩) + 2) \mod 5⟩ \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
24	15 16	opth	$⊢ ⟨0, (y - 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 2) \mod 5⟩)⟩ \leftrightarrow (0 = 0 \land (y - 1) \mod 5 = 2^{nd} (⟨1, (y - 2) \mod 5⟩))$
25	6 7	op2nd	$⊢ 2^{nd} (⟨1, (y - 2) \mod 5⟩) = (y - 2) \mod 5$
26	25	eqeq2i	$⊢ (y - 1) \mod 5 = 2^{nd} (⟨1, (y - 2) \mod 5⟩) \leftrightarrow (y - 1) \mod 5 = (y - 2) \mod 5$
27		5nn	$⊢ 5 \in ℕ$
28	27	nnzi	$⊢ 5 \in ℤ$
29		uzid	$⊢ 5 \in ℤ \to 5 \in ℤ_{\geq 5}$
30	28 29	ax-mp	$⊢ 5 \in ℤ_{\geq 5}$
31		eqid	$⊢ (0 ..^5) = (0 ..^5)$
32	31	modm1nem2	$⊢ (5 \in ℤ_{\geq 5} \land y \in (0 ..^5)) \to (y - 1) \mod 5 \neq (y - 2) \mod 5$
33	30 32	mpan	$⊢ y \in (0 ..^5) \to (y - 1) \mod 5 \neq (y - 2) \mod 5$
34		eqneqall	$⊢ (y - 1) \mod 5 = (y - 2) \mod 5 \to ((y - 1) \mod 5 \neq (y - 2) \mod 5 \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
35	33 34	syl5	$⊢ (y - 1) \mod 5 = (y - 2) \mod 5 \to (y \in (0 ..^5) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
36	26 35	sylbi	$⊢ (y - 1) \mod 5 = 2^{nd} (⟨1, (y - 2) \mod 5⟩) \to (y \in (0 ..^5) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
37	24 36	simplbiim	$⊢ ⟨0, (y - 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 2) \mod 5⟩)⟩ \to (y \in (0 ..^5) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
38	37	com12	$⊢ y \in (0 ..^5) \to (⟨0, (y - 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 2) \mod 5⟩)⟩ \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
39	15 16	opth	$⊢ ⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5⟩ \leftrightarrow (0 = 1 \land (y - 1) \mod 5 = (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5)$
40	20	adantr	$⊢ (0 = 1 \land (y - 1) \mod 5 = (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E$
41	39 40	sylbi	$⊢ ⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5⟩ \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E$
42	41	a1i	$⊢ y \in (0 ..^5) \to (⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5⟩ \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
43	23 38 42	3jaod	$⊢ y \in (0 ..^5) \to ((⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) + 2) \mod 5⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨0, 2^{nd} (⟨1, (y - 2) \mod 5⟩)⟩ \lor ⟨0, (y - 1) \mod 5⟩ = ⟨1, (2^{nd} (⟨1, (y - 2) \mod 5⟩) - 2) \mod 5⟩) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
44	14 43	syld	$⊢ y \in (0 ..^5) \to (\{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E)$
45	44	pm2.01d	$⊢ y \in (0 ..^5) \to \neg \{⟨1, (y - 2) \mod 5⟩, ⟨0, (y - 1) \mod 5⟩\} \in E$

Metamath Proof Explorer

Theorem pgnioedg4

Proof