gpg3nbgrvtx0

Description: In a generalized Petersen graph G , every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-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	gpg3nbgrvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \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	gpgnbgrvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to U = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
6	5	fveq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\|$
7		0ne1	$⊢ 0 \neq 1$
8	7	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 0 \neq 1$
9	8	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (0 \neq 1 \lor (2^{nd} (X) + 1) \mod N \neq 2^{nd} (X))$
10		c0ex	$⊢ 0 \in V$
11		ovex	$⊢ (2^{nd} (X) + 1) \mod N \in V$
12	10 11	opthne	$⊢ ⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \leftrightarrow (0 \neq 1 \lor (2^{nd} (X) + 1) \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) = 0)) \to ⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩$
14		ax-1ne0	$⊢ 1 \neq 0$
15	14	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 1 \neq 0$
16	15	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (1 \neq 0 \lor 2^{nd} (X) \neq (2^{nd} (X) - 1) \mod N)$
17		1ex	$⊢ 1 \in V$
18		fvex	$⊢ 2^{nd} (X) \in V$
19	17 18	opthne	$⊢ ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \leftrightarrow (1 \neq 0 \lor 2^{nd} (X) \neq (2^{nd} (X) - 1) \mod N)$
20	16 19	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩$
21		simpl	$⊢ (X \in V \land 1^{st} (X) = 0) \to X \in V$
22	21	anim2i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V)$
23		eqid	$⊢ (0 ..^N) = (0 ..^N)$
24	23 1 2 3	gpgvtxel2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to 2^{nd} (X) \in (0 ..^N)$
25		elfzoelz	$⊢ 2^{nd} (X) \in (0 ..^N) \to 2^{nd} (X) \in ℤ$
26	22 24 25	3syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) \in ℤ$
27	26	zcnd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) \in ℂ$
28		1cnd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 1 \in ℂ$
29		2cnd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2 \in ℂ$
30	27 28 29	subadd23d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) - 1 + 2 = 2^{nd} (X) + 2 - 1$
31		2m1e1	$⊢ 2 - 1 = 1$
32	31	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2 - 1 = 1$
33	32	oveq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) + 2 - 1 = 2^{nd} (X) + 1$
34	30 33	eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) - 1 + 2 = 2^{nd} (X) + 1$
35	34	eqcomd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) + 1 = 2^{nd} (X) - 1 + 2$
36	35	oveq1d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) + 1) \mod N = (2^{nd} (X) - 1 + 2) \mod N$
37		1zzd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 1 \in ℤ$
38	26 37	zsubcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) - 1 \in ℤ$
39	38	zred	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) - 1 \in ℝ$
40		2re	$⊢ 2 \in ℝ$
41	40	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2 \in ℝ$
42		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
43	42	nnrpd	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ^{+}$
44	43	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to N \in ℝ^{+}$
45		modaddabs	$⊢ (2^{nd} (X) - 1 \in ℝ \land 2 \in ℝ \land N \in ℝ^{+}) \to (((2^{nd} (X) - 1) \mod N) + (2 \mod N)) \mod N = (2^{nd} (X) - 1 + 2) \mod N$
46	39 41 44 45	syl3anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (((2^{nd} (X) - 1) \mod N) + (2 \mod N)) \mod N = (2^{nd} (X) - 1 + 2) \mod N$
47	46	eqcomd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) - 1 + 2) \mod N = (((2^{nd} (X) - 1) \mod N) + (2 \mod N)) \mod N$
48	36 47	eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) + 1) \mod N = (((2^{nd} (X) - 1) \mod N) + (2 \mod N)) \mod N$
49	42	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to N \in ℕ$
50	38 49	zmodcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) - 1) \mod N \in ℕ_{0}$
51		modlt	$⊢ (2^{nd} (X) - 1 \in ℝ \land N \in ℝ^{+}) \to (2^{nd} (X) - 1) \mod N < N$
52	39 44 51	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) - 1) \mod N < N$
53	50 52	jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ((2^{nd} (X) - 1) \mod N \in ℕ_{0} \land (2^{nd} (X) - 1) \mod N < N)$
54		2nn0	$⊢ 2 \in ℕ_{0}$
55	54	a1i	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℕ_{0}$
56		eluz2	$⊢ N \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land N \in ℤ \land 3 \leq N)$
57	40	a1i	$⊢ (N \in ℤ \land 3 \leq N) \to 2 \in ℝ$
58		3re	$⊢ 3 \in ℝ$
59	58	a1i	$⊢ (N \in ℤ \land 3 \leq N) \to 3 \in ℝ$
60		zre	$⊢ N \in ℤ \to N \in ℝ$
61	60	adantr	$⊢ (N \in ℤ \land 3 \leq N) \to N \in ℝ$
62		2lt3	$⊢ 2 < 3$
63	62	a1i	$⊢ (N \in ℤ \land 3 \leq N) \to 2 < 3$
64		simpr	$⊢ (N \in ℤ \land 3 \leq N) \to 3 \leq N$
65	57 59 61 63 64	ltletrd	$⊢ (N \in ℤ \land 3 \leq N) \to 2 < N$
66	65	3adant1	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to 2 < N$
67	56 66	sylbi	$⊢ N \in ℤ_{\geq 3} \to 2 < N$
68		elfzo0	$⊢ 2 \in (0 ..^N) \leftrightarrow (2 \in ℕ_{0} \land N \in ℕ \land 2 < N)$
69	55 42 67 68	syl3anbrc	$⊢ N \in ℤ_{\geq 3} \to 2 \in (0 ..^N)$
70		zmodidfzoimp	$⊢ 2 \in (0 ..^N) \to 2 \mod N = 2$
71	69 70	syl	$⊢ N \in ℤ_{\geq 3} \to 2 \mod N = 2$
72		2nn	$⊢ 2 \in ℕ$
73	71 72	eqeltrdi	$⊢ N \in ℤ_{\geq 3} \to 2 \mod N \in ℕ$
74	40	a1i	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℝ$
75		modlt	$⊢ (2 \in ℝ \land N \in ℝ^{+}) \to 2 \mod N < N$
76	74 43 75	syl2anc	$⊢ N \in ℤ_{\geq 3} \to 2 \mod N < N$
77	73 76	jca	$⊢ N \in ℤ_{\geq 3} \to (2 \mod N \in ℕ \land 2 \mod N < N)$
78	77	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2 \mod N \in ℕ \land 2 \mod N < N)$
79		addmodne	$⊢ (N \in ℕ \land ((2^{nd} (X) - 1) \mod N \in ℕ_{0} \land (2^{nd} (X) - 1) \mod N < N) \land (2 \mod N \in ℕ \land 2 \mod N < N)) \to (((2^{nd} (X) - 1) \mod N) + (2 \mod N)) \mod N \neq (2^{nd} (X) - 1) \mod N$
80	49 53 78 79	syl3anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (((2^{nd} (X) - 1) \mod N) + (2 \mod N)) \mod N \neq (2^{nd} (X) - 1) \mod N$
81	48 80	eqnetrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) + 1) \mod N \neq (2^{nd} (X) - 1) \mod N$
82	81	necomd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) - 1) \mod N \neq (2^{nd} (X) + 1) \mod N$
83	82	olcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (0 \neq 0 \lor (2^{nd} (X) - 1) \mod N \neq (2^{nd} (X) + 1) \mod N)$
84		ovex	$⊢ (2^{nd} (X) - 1) \mod N \in V$
85	10 84	opthne	$⊢ ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩ \leftrightarrow (0 \neq 0 \lor (2^{nd} (X) - 1) \mod N \neq (2^{nd} (X) + 1) \mod N)$
86	83 85	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩$
87	13 20 86	3jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \land ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩)$
88		opex	$⊢ ⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V$
89		opex	$⊢ ⟨1, 2^{nd} (X)⟩ \in V$
90		opex	$⊢ ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V$
91		hashtpg	$⊢ (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V) \to ((⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \land ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩) \leftrightarrow \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\| = 3)$
92	88 89 90 91	mp3an	$⊢ (⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \land ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩) \leftrightarrow \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\| = 3$
93	87 92	sylib	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\| = 3$
94	6 93	eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = 3$

Metamath Proof Explorer

Theorem gpg3nbgrvtx0

Proof