gpg5nbgrvtx03star

Description: In a generalized Petersen graph G(N,K) of order greater than 8 ( 3 < N ), every outside vertex has exactly three (different) neighbors, and none of these neighbors are connected by an edge (i.e., the (closed) neighborhood of every outside vertex induces a subgraph which is isomorphic to a 3-star). (Contributed by AV, 31-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$
	gpgnbgr.e	$⊢ E = Edg (G)$
Assertion	gpg5nbgrvtx03star	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)$

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		gpgnbgr.e	$⊢ E = Edg (G)$
6		uzuzle34	$⊢ N \in ℤ_{\geq 4} \to N \in ℤ_{\geq 3}$
7	1 2 3 4	gpg3nbgrvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = 3$
8	6 7	sylanl1	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = 3$
9		eqid	$⊢ ⟨0, (2^{nd} (X) + 1) \mod N⟩ = ⟨0, (2^{nd} (X) + 1) \mod N⟩$
10	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
11	10	biimpi	$⊢ K \in J \to K \in (1 ..^⌈\frac{N}{2}⌉)$
12		gpgusgra	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) with typecode \|-
13	2 12	eqeltrid	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to G \in USGraph$
14	6 11 13	syl2an	$⊢ (N \in ℤ_{\geq 4} \land K \in J) \to G \in USGraph$
15	14	adantr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to G \in USGraph$
16	5	usgredgne	$⊢ (G \in USGraph \land \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E) \to ⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩$
17	16	neneqd	$⊢ (G \in USGraph \land \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E) \to \neg ⟨0, (2^{nd} (X) + 1) \mod N⟩ = ⟨0, (2^{nd} (X) + 1) \mod N⟩$
18	17	ex	$⊢ G \in USGraph \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \to \neg ⟨0, (2^{nd} (X) + 1) \mod N⟩ = ⟨0, (2^{nd} (X) + 1) \mod N⟩)$
19	15 18	syl	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \to \neg ⟨0, (2^{nd} (X) + 1) \mod N⟩ = ⟨0, (2^{nd} (X) + 1) \mod N⟩)$
20	9 19	mt2i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \neg \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E$
21		df-nel	$⊢ \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \leftrightarrow \neg \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E$
22	20 21	sylibr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E$
23	6	adantr	$⊢ (N \in ℤ_{\geq 4} \land K \in J) \to N \in ℤ_{\geq 3}$
24	23	adantr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to N \in ℤ_{\geq 3}$
25		simplr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to K \in J$
26	6	anim1i	$⊢ (N \in ℤ_{\geq 4} \land K \in J) \to (N \in ℤ_{\geq 3} \land K \in J)$
27		simpl	$⊢ (X \in V \land 1^{st} (X) = 0) \to X \in V$
28	26 27	anim12i	$⊢ ((N \in ℤ_{\geq 4} \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)$
29		eqid	$⊢ (0 ..^N) = (0 ..^N)$
30	29 1 2 3	gpgvtxel2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to 2^{nd} (X) \in (0 ..^N)$
31	28 30	syl	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) \in (0 ..^N)$
32	1 2 3 5	gpg5nbgrvtx03starlem1	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land 2^{nd} (X) \in (0 ..^N)) \to \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E$
33	24 25 31 32	syl3anc	$⊢ ((N \in ℤ_{\geq 4} \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)⟩\} \notin E$
34		simpll	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to N \in ℤ_{\geq 4}$
35		elfzoelz	$⊢ 2^{nd} (X) \in (0 ..^N) \to 2^{nd} (X) \in ℤ$
36	28 30 35	3syl	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) \in ℤ$
37	1 2 3 5	gpg5nbgrvtx03starlem2	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land 2^{nd} (X) \in ℤ) \to \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E$
38	34 25 36 37	syl3anc	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E$
39		opex	$⊢ ⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V$
40		opex	$⊢ ⟨1, 2^{nd} (X)⟩ \in V$
41		opex	$⊢ ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V$
42		preq2	$⊢ y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\}$
43		neleq1	$⊢ \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E)$
44	42 43	syl	$⊢ y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E)$
45		preq2	$⊢ y = ⟨1, 2^{nd} (X)⟩ \to \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\}$
46		neleq1	$⊢ \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E)$
47	45 46	syl	$⊢ y = ⟨1, 2^{nd} (X)⟩ \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E)$
48		preq2	$⊢ y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
49		neleq1	$⊢ \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
50	48 49	syl	$⊢ y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
51	39 40 41 44 47 50	raltp	$⊢ \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \leftrightarrow (\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \land \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E \land \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
52	22 33 38 51	syl3anbrc	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E$
53		prcom	$⊢ \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\}$
54		neleq1	$⊢ \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \to (\{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E)$
55	53 54	ax-mp	$⊢ \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E$
56	33 55	sylibr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E$
57		eqid	$⊢ ⟨1, 2^{nd} (X)⟩ = ⟨1, 2^{nd} (X)⟩$
58	5	usgredgne	$⊢ (G \in USGraph \land \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \in E) \to ⟨1, 2^{nd} (X)⟩ \neq ⟨1, 2^{nd} (X)⟩$
59	58	neneqd	$⊢ (G \in USGraph \land \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \in E) \to \neg ⟨1, 2^{nd} (X)⟩ = ⟨1, 2^{nd} (X)⟩$
60	59	ex	$⊢ G \in USGraph \to (\{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \in E \to \neg ⟨1, 2^{nd} (X)⟩ = ⟨1, 2^{nd} (X)⟩)$
61	15 60	syl	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \in E \to \neg ⟨1, 2^{nd} (X)⟩ = ⟨1, 2^{nd} (X)⟩)$
62	57 61	mt2i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \neg \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \in E$
63		df-nel	$⊢ \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \notin E \leftrightarrow \neg \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \in E$
64	62 63	sylibr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \notin E$
65	1 2 3 5	gpg5nbgrvtx03starlem3	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land 2^{nd} (X) \in (0 ..^N)) \to \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E$
66	24 25 31 65	syl3anc	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E$
67		preq2	$⊢ y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to \{⟨1, 2^{nd} (X)⟩, y\} = \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\}$
68		neleq1	$⊢ \{⟨1, 2^{nd} (X)⟩, y\} = \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \to (\{⟨1, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E)$
69	67 68	syl	$⊢ y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (\{⟨1, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E)$
70		preq2	$⊢ y = ⟨1, 2^{nd} (X)⟩ \to \{⟨1, 2^{nd} (X)⟩, y\} = \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\}$
71		neleq1	$⊢ \{⟨1, 2^{nd} (X)⟩, y\} = \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \to (\{⟨1, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \notin E)$
72	70 71	syl	$⊢ y = ⟨1, 2^{nd} (X)⟩ \to (\{⟨1, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \notin E)$
73		preq2	$⊢ y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to \{⟨1, 2^{nd} (X)⟩, y\} = \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
74		neleq1	$⊢ \{⟨1, 2^{nd} (X)⟩, y\} = \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \to (\{⟨1, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
75	73 74	syl	$⊢ y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (\{⟨1, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
76	39 40 41 69 72 75	raltp	$⊢ \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨1, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow (\{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \land \{⟨1, 2^{nd} (X)⟩, ⟨1, 2^{nd} (X)⟩\} \notin E \land \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
77	56 64 66 76	syl3anbrc	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨1, 2^{nd} (X)⟩, y\} \notin E$
78		prcom	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
79		neleq1	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
80	78 79	ax-mp	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E$
81	38 80	sylibr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E$
82		prcom	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} = \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
83		neleq1	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} = \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
84	82 83	ax-mp	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E$
85	66 84	sylibr	$⊢ ((N \in ℤ_{\geq 4} \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)⟩\} \notin E$
86		eqid	$⊢ ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (2^{nd} (X) - 1) \mod N⟩$
87	5	usgredgne	$⊢ (G \in USGraph \land \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E) \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩$
88	87	neneqd	$⊢ (G \in USGraph \land \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E) \to \neg ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (2^{nd} (X) - 1) \mod N⟩$
89	88	ex	$⊢ G \in USGraph \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E \to \neg ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
90	15 89	syl	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E \to \neg ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
91	86 90	mt2i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \neg \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E$
92		df-nel	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E \leftrightarrow \neg \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E$
93	91 92	sylibr	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E$
94		preq2	$⊢ y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\}$
95		neleq1	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E)$
96	94 95	syl	$⊢ y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E)$
97		preq2	$⊢ y = ⟨1, 2^{nd} (X)⟩ \to \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\}$
98		neleq1	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E)$
99	97 98	syl	$⊢ y = ⟨1, 2^{nd} (X)⟩ \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E)$
100		preq2	$⊢ y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
101		neleq1	$⊢ \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
102	100 101	syl	$⊢ y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
103	39 40 41 96 99 102	raltp	$⊢ \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E \leftrightarrow (\{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \notin E \land \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩\} \notin E \land \{⟨0, (2^{nd} (X) - 1) \mod N⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \notin E)$
104	81 85 93 103	syl3anbrc	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E$
105		preq1	$⊢ x = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to \{x, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\}$
106		neleq1	$⊢ \{x, y\} = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \to (\{x, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E)$
107	105 106	syl	$⊢ x = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (\{x, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E)$
108	107	ralbidv	$⊢ x = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \to (\forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E)$
109		preq1	$⊢ x = ⟨1, 2^{nd} (X)⟩ \to \{x, y\} = \{⟨1, 2^{nd} (X)⟩, y\}$
110		neleq1	$⊢ \{x, y\} = \{⟨1, 2^{nd} (X)⟩, y\} \to (\{x, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, y\} \notin E)$
111	109 110	syl	$⊢ x = ⟨1, 2^{nd} (X)⟩ \to (\{x, y\} \notin E \leftrightarrow \{⟨1, 2^{nd} (X)⟩, y\} \notin E)$
112	111	ralbidv	$⊢ x = ⟨1, 2^{nd} (X)⟩ \to (\forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨1, 2^{nd} (X)⟩, y\} \notin E)$
113		preq1	$⊢ x = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to \{x, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\}$
114		neleq1	$⊢ \{x, y\} = \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \to (\{x, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E)$
115	113 114	syl	$⊢ x = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (\{x, y\} \notin E \leftrightarrow \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E)$
116	115	ralbidv	$⊢ x = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \to (\forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E)$
117	39 40 41 108 112 116	raltp	$⊢ \forall x \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{x, y\} \notin E \leftrightarrow (\forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) + 1) \mod N⟩, y\} \notin E \land \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨1, 2^{nd} (X)⟩, y\} \notin E \land \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{⟨0, (2^{nd} (X) - 1) \mod N⟩, y\} \notin E)$
118	52 77 104 117	syl3anbrc	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \forall x \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{x, y\} \notin E$
119	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⟩\}$
120	6 119	sylanl1	$⊢ ((N \in ℤ_{\geq 4} \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⟩\}$
121	120	raleqdv	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\forall y \in U \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{x, y\} \notin E)$
122	120 121	raleqbidvv	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\forall x \in U \forall y \in U \{x, y\} \notin E \leftrightarrow \forall x \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \forall y \in \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \{x, y\} \notin E)$
123	118 122	mpbird	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \forall x \in U \forall y \in U \{x, y\} \notin E$
124	8 123	jca	$⊢ ((N \in ℤ_{\geq 4} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)$

Metamath Proof Explorer

Theorem gpg5nbgrvtx03star

Proof