gpg3nbgrvtx1

Description: In a generalized Petersen graph G , every inside vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025) (Proof shortened by AV, 22-Nov-2025)

	Ref	Expression
Hypotheses	gpgnbgr.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgnbgr.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpgnbgr.v	$⊢ V = Vtx (G)$
	gpgnbgr.u	$⊢ U = G NeighbVtx X$
Assertion	gpg3nbgrvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \|U\| = 3$

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgnbgr.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
3		gpgnbgr.v	$⊢ V = Vtx (G)$
4		gpgnbgr.u	$⊢ U = G NeighbVtx X$
5	1 2 3 4	gpgnbgrvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to U = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}$
6	5	fveq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \|U\| = \|\{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}\|$
7		ax-1ne0	$⊢ 1 \neq 0$
8	7	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to 1 \neq 0$
9	8	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (1 \neq 0 \lor (2^{nd} (X) + K) \mod N \neq 2^{nd} (X))$
10		1ex	$⊢ 1 \in V$
11		ovex	$⊢ (2^{nd} (X) + K) \mod N \in V$
12	10 11	opthne	$⊢ ⟨1, (2^{nd} (X) + K) \mod N⟩ \neq ⟨0, 2^{nd} (X)⟩ \leftrightarrow (1 \neq 0 \lor (2^{nd} (X) + K) \mod N \neq 2^{nd} (X))$
13	9 12	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to ⟨1, (2^{nd} (X) + K) \mod N⟩ \neq ⟨0, 2^{nd} (X)⟩$
14		0ne1	$⊢ 0 \neq 1$
15	14	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to 0 \neq 1$
16	15	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (0 \neq 1 \lor 2^{nd} (X) \neq (2^{nd} (X) - K) \mod N)$
17		c0ex	$⊢ 0 \in V$
18		fvex	$⊢ 2^{nd} (X) \in V$
19	17 18	opthne	$⊢ ⟨0, 2^{nd} (X)⟩ \neq ⟨1, (2^{nd} (X) - K) \mod N⟩ \leftrightarrow (0 \neq 1 \lor 2^{nd} (X) \neq (2^{nd} (X) - K) \mod N)$
20	16 19	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to ⟨0, 2^{nd} (X)⟩ \neq ⟨1, (2^{nd} (X) - K) \mod N⟩$
21		simpll	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to N \in ℤ_{\geq 3}$
22		eqid	$⊢ (0 ..^N) = (0 ..^N)$
23	22 1 2 3	gpgvtxel2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to 2^{nd} (X) \in (0 ..^N)$
24	23	adantrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to 2^{nd} (X) \in (0 ..^N)$
25		simplr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to K \in J$
26	1 22	modmknepk	$⊢ (N \in ℤ_{\geq 3} \land 2^{nd} (X) \in (0 ..^N) \land K \in J) \to (2^{nd} (X) - K) \mod N \neq (2^{nd} (X) + K) \mod N$
27	21 24 25 26	syl3anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (2^{nd} (X) - K) \mod N \neq (2^{nd} (X) + K) \mod N$
28	27	olcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (1 \neq 1 \lor (2^{nd} (X) - K) \mod N \neq (2^{nd} (X) + K) \mod N)$
29		ovex	$⊢ (2^{nd} (X) - K) \mod N \in V$
30	10 29	opthne	$⊢ ⟨1, (2^{nd} (X) - K) \mod N⟩ \neq ⟨1, (2^{nd} (X) + K) \mod N⟩ \leftrightarrow (1 \neq 1 \lor (2^{nd} (X) - K) \mod N \neq (2^{nd} (X) + K) \mod N)$
31	28 30	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to ⟨1, (2^{nd} (X) - K) \mod N⟩ \neq ⟨1, (2^{nd} (X) + K) \mod N⟩$
32	13 20 31	3jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \neq ⟨0, 2^{nd} (X)⟩ \land ⟨0, 2^{nd} (X)⟩ \neq ⟨1, (2^{nd} (X) - K) \mod N⟩ \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \neq ⟨1, (2^{nd} (X) + K) \mod N⟩)$
33		opex	$⊢ ⟨1, (2^{nd} (X) + K) \mod N⟩ \in V$
34		opex	$⊢ ⟨0, 2^{nd} (X)⟩ \in V$
35		opex	$⊢ ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V$
36		hashtpg	$⊢ (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V) \to ((⟨1, (2^{nd} (X) + K) \mod N⟩ \neq ⟨0, 2^{nd} (X)⟩ \land ⟨0, 2^{nd} (X)⟩ \neq ⟨1, (2^{nd} (X) - K) \mod N⟩ \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \neq ⟨1, (2^{nd} (X) + K) \mod N⟩) \leftrightarrow \|\{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}\| = 3)$
37	33 34 35 36	mp3an	$⊢ (⟨1, (2^{nd} (X) + K) \mod N⟩ \neq ⟨0, 2^{nd} (X)⟩ \land ⟨0, 2^{nd} (X)⟩ \neq ⟨1, (2^{nd} (X) - K) \mod N⟩ \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \neq ⟨1, (2^{nd} (X) + K) \mod N⟩) \leftrightarrow \|\{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}\| = 3$
38	32 37	sylib	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \|\{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}\| = 3$
39	6 38	eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \|U\| = 3$

Metamath Proof Explorer

Theorem gpg3nbgrvtx1

Proof