gpg3nbgrvtx1

Description: In a generalized Petersen graph G , every inside vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-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	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
23	22	biimpi	$⊢ K \in J \to K \in (1 ..^⌈\frac{N}{2}⌉)$
24	23	ad2antlr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to K \in (1 ..^⌈\frac{N}{2}⌉)$
25		eqid	$⊢ (0 ..^N) = (0 ..^N)$
26	25 1 2 3	gpgvtxel2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to 2^{nd} (X) \in (0 ..^N)$
27	26	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)$
28		gpg3nbgrvtxlem	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉) \land 2^{nd} (X) \in (0 ..^N)) \to (2^{nd} (X) + K) \mod N \neq (2^{nd} (X) - K) \mod N$
29	21 24 27 28	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$
30	29	necomd	$⊢ ((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$
31	30	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)$
32		ovex	$⊢ (2^{nd} (X) - K) \mod N \in V$
33	10 32	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)$
34	31 33	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⟩$
35	13 20 34	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⟩)$
36		opex	$⊢ ⟨1, (2^{nd} (X) + K) \mod N⟩ \in V$
37		opex	$⊢ ⟨0, 2^{nd} (X)⟩ \in V$
38		opex	$⊢ ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V$
39		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)$
40	36 37 38 39	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$
41	35 40	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$
42	6 41	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