gpg5nbgr3star

Description: In a generalized Petersen graph G(N,K) of order 10 ( N = 5 ), these are the Petersen graph G(5,2) and the 5-prism G(5,1), every vertex has exactly three (different) neighbors, and none of these neighbors are connected by an edge (i.e., the (closed) neighborhood of every vertex induces a subgraph which is isomorphic to a 3-star). This does not hold for every generalized Petersen graph: for example, in the 3-prism G(3,1) (see gpg31grim3prism TODO) and the Dürer graph G(6,2) there are vertices which have neighborhoods containing triangles. In general, all generalized Peterson graphs G(N,K) with N = 3 x. K contain triangles, see gpg3kgrtriex . (Contributed by AV, 8-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$
	gpgnbgr.e	$⊢ E = Edg (G)$
Assertion	gpg5nbgr3star	$⊢ (N = 5 \land K \in J \land X \in V) \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		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
7		eleq1	$⊢ N = 5 \to (N \in ℤ_{\geq 3} \leftrightarrow 5 \in ℤ_{\geq 3})$
8	6 7	mpbiri	$⊢ N = 5 \to N \in ℤ_{\geq 3}$
9	8	anim1i	$⊢ (N = 5 \land K \in J) \to (N \in ℤ_{\geq 3} \land K \in J)$
10		eqid	$⊢ (0 ..^N) = (0 ..^N)$
11	10 1 2 3	gpgvtxel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \leftrightarrow \exists a \in \{0, 1\} \exists b \in (0 ..^N) X = ⟨a, b⟩)$
12	9 11	syl	$⊢ (N = 5 \land K \in J) \to (X \in V \leftrightarrow \exists a \in \{0, 1\} \exists b \in (0 ..^N) X = ⟨a, b⟩)$
13	12	biimp3a	$⊢ (N = 5 \land K \in J \land X \in V) \to \exists a \in \{0, 1\} \exists b \in (0 ..^N) X = ⟨a, b⟩$
14		elpri	$⊢ a \in \{0, 1\} \to (a = 0 \lor a = 1)$
15		opeq1	$⊢ a = 0 \to ⟨a, b⟩ = ⟨0, b⟩$
16	15	eqeq2d	$⊢ a = 0 \to (X = ⟨a, b⟩ \leftrightarrow X = ⟨0, b⟩)$
17	16	adantr	$⊢ (a = 0 \land (N = 5 \land K \in J \land X \in V)) \to (X = ⟨a, b⟩ \leftrightarrow X = ⟨0, b⟩)$
18		c0ex	$⊢ 0 \in V$
19		vex	$⊢ b \in V$
20	18 19	op1std	$⊢ X = ⟨0, b⟩ \to 1^{st} (X) = 0$
21		4z	$⊢ 4 \in ℤ$
22		5nn	$⊢ 5 \in ℕ$
23	22	nnzi	$⊢ 5 \in ℤ$
24		4re	$⊢ 4 \in ℝ$
25		5re	$⊢ 5 \in ℝ$
26		4lt5	$⊢ 4 < 5$
27	24 25 26	ltleii	$⊢ 4 \leq 5$
28		eluz2	$⊢ 5 \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land 5 \in ℤ \land 4 \leq 5)$
29	21 23 27 28	mpbir3an	$⊢ 5 \in ℤ_{\geq 4}$
30		eleq1	$⊢ N = 5 \to (N \in ℤ_{\geq 4} \leftrightarrow 5 \in ℤ_{\geq 4})$
31	29 30	mpbiri	$⊢ N = 5 \to N \in ℤ_{\geq 4}$
32	1 2 3 4 5	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)$
33	31 32	sylanl1	$⊢ ((N = 5 \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)$
34	33	exp43	$⊢ N = 5 \to (K \in J \to (X \in V \to (1^{st} (X) = 0 \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))))$
35	34	3imp	$⊢ (N = 5 \land K \in J \land X \in V) \to (1^{st} (X) = 0 \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
36	20 35	syl5	$⊢ (N = 5 \land K \in J \land X \in V) \to (X = ⟨0, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
37	36	adantl	$⊢ (a = 0 \land (N = 5 \land K \in J \land X \in V)) \to (X = ⟨0, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
38	17 37	sylbid	$⊢ (a = 0 \land (N = 5 \land K \in J \land X \in V)) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
39	38	ex	$⊢ a = 0 \to ((N = 5 \land K \in J \land X \in V) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)))$
40		opeq1	$⊢ a = 1 \to ⟨a, b⟩ = ⟨1, b⟩$
41	40	eqeq2d	$⊢ a = 1 \to (X = ⟨a, b⟩ \leftrightarrow X = ⟨1, b⟩)$
42	41	adantr	$⊢ (a = 1 \land (N = 5 \land K \in J \land X \in V)) \to (X = ⟨a, b⟩ \leftrightarrow X = ⟨1, b⟩)$
43		1ex	$⊢ 1 \in V$
44	43 19	op1std	$⊢ X = ⟨1, b⟩ \to 1^{st} (X) = 1$
45	1 2 3 4	gpg3nbgrvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \|U\| = 3$
46	8 45	sylanl1	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \|U\| = 3$
47		eqid	$⊢ ⟨1, (2^{nd} (X) + K) \mod N⟩ = ⟨1, (2^{nd} (X) + K) \mod N⟩$
48	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
49	48	biimpi	$⊢ K \in J \to K \in (1 ..^⌈\frac{N}{2}⌉)$
50		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 \|-
51	2 50	eqeltrid	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to G \in USGraph$
52	8 49 51	syl2an	$⊢ (N = 5 \land K \in J) \to G \in USGraph$
53	52	adantr	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to G \in USGraph$
54	5	usgredgne	$⊢ (G \in USGraph \land \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E) \to ⟨1, (2^{nd} (X) + K) \mod N⟩ \neq ⟨1, (2^{nd} (X) + K) \mod N⟩$
55	54	neneqd	$⊢ (G \in USGraph \land \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E) \to \neg ⟨1, (2^{nd} (X) + K) \mod N⟩ = ⟨1, (2^{nd} (X) + K) \mod N⟩$
56	55	ex	$⊢ G \in USGraph \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \to \neg ⟨1, (2^{nd} (X) + K) \mod N⟩ = ⟨1, (2^{nd} (X) + K) \mod N⟩)$
57	53 56	syl	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \to \neg ⟨1, (2^{nd} (X) + K) \mod N⟩ = ⟨1, (2^{nd} (X) + K) \mod N⟩)$
58	47 57	mt2i	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \neg \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E$
59		df-nel	$⊢ \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \leftrightarrow \neg \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E$
60	58 59	sylibr	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E$
61		fvexd	$⊢ (X \in V \land 1^{st} (X) = 1) \to 2^{nd} (X) \in V$
62	1 2 3 5	gpg5nbgrvtx13starlem1	$⊢ ((N = 5 \land K \in J) \land 2^{nd} (X) \in V) \to \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E$
63	61 62	sylan2	$⊢ ((N = 5 \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)⟩\} \notin E$
64		simpl	$⊢ (X \in V \land 1^{st} (X) = 1) \to X \in V$
65	9 64	anim12i	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V)$
66	10 1 2 3	gpgvtxel2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to 2^{nd} (X) \in (0 ..^N)$
67		elfzoelz	$⊢ 2^{nd} (X) \in (0 ..^N) \to 2^{nd} (X) \in ℤ$
68	65 66 67	3syl	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to 2^{nd} (X) \in ℤ$
69	1 2 3 5	gpg5nbgrvtx13starlem2	$⊢ ((N = 5 \land K \in J) \land 2^{nd} (X) \in ℤ) \to \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E$
70	68 69	syldan	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E$
71		opex	$⊢ ⟨1, (2^{nd} (X) + K) \mod N⟩ \in V$
72		opex	$⊢ ⟨0, 2^{nd} (X)⟩ \in V$
73		opex	$⊢ ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V$
74		preq2	$⊢ y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\}$
75		neleq1	$⊢ \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E)$
76	74 75	syl	$⊢ y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E)$
77		preq2	$⊢ y = ⟨0, 2^{nd} (X)⟩ \to \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\}$
78		neleq1	$⊢ \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E)$
79	77 78	syl	$⊢ y = ⟨0, 2^{nd} (X)⟩ \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E)$
80		preq2	$⊢ y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}$
81		neleq1	$⊢ \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
82	80 81	syl	$⊢ y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to (\{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
83	71 72 73 76 79 82	raltp	$⊢ \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \leftrightarrow (\{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \land \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E \land \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
84	60 63 70 83	syl3anbrc	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E$
85		prcom	$⊢ \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\}$
86		neleq1	$⊢ \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \to (\{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E)$
87	85 86	ax-mp	$⊢ \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E$
88	63 87	sylibr	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E$
89		eqid	$⊢ ⟨0, 2^{nd} (X)⟩ = ⟨0, 2^{nd} (X)⟩$
90	5	usgredgne	$⊢ (G \in USGraph \land \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \in E) \to ⟨0, 2^{nd} (X)⟩ \neq ⟨0, 2^{nd} (X)⟩$
91	90	neneqd	$⊢ (G \in USGraph \land \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \in E) \to \neg ⟨0, 2^{nd} (X)⟩ = ⟨0, 2^{nd} (X)⟩$
92	91	ex	$⊢ G \in USGraph \to (\{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \in E \to \neg ⟨0, 2^{nd} (X)⟩ = ⟨0, 2^{nd} (X)⟩)$
93	53 92	syl	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \in E \to \neg ⟨0, 2^{nd} (X)⟩ = ⟨0, 2^{nd} (X)⟩)$
94	89 93	mt2i	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \neg \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \in E$
95		df-nel	$⊢ \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \notin E \leftrightarrow \neg \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \in E$
96	94 95	sylibr	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \notin E$
97	1 2 3 5	gpg5nbgrvtx13starlem3	$⊢ ((N = 5 \land K \in J) \land 2^{nd} (X) \in V) \to \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E$
98	61 97	sylan2	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E$
99		preq2	$⊢ y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to \{⟨0, 2^{nd} (X)⟩, y\} = \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\}$
100		neleq1	$⊢ \{⟨0, 2^{nd} (X)⟩, y\} = \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \to (\{⟨0, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E)$
101	99 100	syl	$⊢ y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to (\{⟨0, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E)$
102		preq2	$⊢ y = ⟨0, 2^{nd} (X)⟩ \to \{⟨0, 2^{nd} (X)⟩, y\} = \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\}$
103		neleq1	$⊢ \{⟨0, 2^{nd} (X)⟩, y\} = \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \to (\{⟨0, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \notin E)$
104	102 103	syl	$⊢ y = ⟨0, 2^{nd} (X)⟩ \to (\{⟨0, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \notin E)$
105		preq2	$⊢ y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to \{⟨0, 2^{nd} (X)⟩, y\} = \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}$
106		neleq1	$⊢ \{⟨0, 2^{nd} (X)⟩, y\} = \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \to (\{⟨0, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
107	105 106	syl	$⊢ y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to (\{⟨0, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
108	71 72 73 101 104 107	raltp	$⊢ \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨0, 2^{nd} (X)⟩, y\} \notin E \leftrightarrow (\{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \land \{⟨0, 2^{nd} (X)⟩, ⟨0, 2^{nd} (X)⟩\} \notin E \land \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
109	88 96 98 108	syl3anbrc	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨0, 2^{nd} (X)⟩, y\} \notin E$
110		prcom	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}$
111		neleq1	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
112	110 111	ax-mp	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E$
113	70 112	sylibr	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E$
114		prcom	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} = \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}$
115		neleq1	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} = \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
116	114 115	ax-mp	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E$
117	98 116	sylibr	$⊢ ((N = 5 \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)⟩\} \notin E$
118		eqid	$⊢ ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (2^{nd} (X) - K) \mod N⟩$
119	5	usgredgne	$⊢ (G \in USGraph \land \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E) \to ⟨1, (2^{nd} (X) - K) \mod N⟩ \neq ⟨1, (2^{nd} (X) - K) \mod N⟩$
120	119	neneqd	$⊢ (G \in USGraph \land \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E) \to \neg ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (2^{nd} (X) - K) \mod N⟩$
121	120	ex	$⊢ G \in USGraph \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E \to \neg ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (2^{nd} (X) - K) \mod N⟩)$
122	53 121	syl	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E \to \neg ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (2^{nd} (X) - K) \mod N⟩)$
123	118 122	mt2i	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \neg \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E$
124		df-nel	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E \leftrightarrow \neg \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E$
125	123 124	sylibr	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E$
126		preq2	$⊢ y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\}$
127		neleq1	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E)$
128	126 127	syl	$⊢ y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E)$
129		preq2	$⊢ y = ⟨0, 2^{nd} (X)⟩ \to \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\}$
130		neleq1	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E)$
131	129 130	syl	$⊢ y = ⟨0, 2^{nd} (X)⟩ \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E)$
132		preq2	$⊢ y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\}$
133		neleq1	$⊢ \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
134	132 133	syl	$⊢ y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to (\{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
135	71 72 73 128 131 134	raltp	$⊢ \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E \leftrightarrow (\{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \notin E \land \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨0, 2^{nd} (X)⟩\} \notin E \land \{⟨1, (2^{nd} (X) - K) \mod N⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \notin E)$
136	113 117 125 135	syl3anbrc	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E$
137		preq1	$⊢ x = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to \{x, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\}$
138		neleq1	$⊢ \{x, y\} = \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \to (\{x, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E)$
139	137 138	syl	$⊢ x = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to (\{x, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E)$
140	139	ralbidv	$⊢ x = ⟨1, (2^{nd} (X) + K) \mod N⟩ \to (\forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E)$
141		preq1	$⊢ x = ⟨0, 2^{nd} (X)⟩ \to \{x, y\} = \{⟨0, 2^{nd} (X)⟩, y\}$
142		neleq1	$⊢ \{x, y\} = \{⟨0, 2^{nd} (X)⟩, y\} \to (\{x, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, y\} \notin E)$
143	141 142	syl	$⊢ x = ⟨0, 2^{nd} (X)⟩ \to (\{x, y\} \notin E \leftrightarrow \{⟨0, 2^{nd} (X)⟩, y\} \notin E)$
144	143	ralbidv	$⊢ x = ⟨0, 2^{nd} (X)⟩ \to (\forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨0, 2^{nd} (X)⟩, y\} \notin E)$
145		preq1	$⊢ x = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to \{x, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\}$
146		neleq1	$⊢ \{x, y\} = \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \to (\{x, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E)$
147	145 146	syl	$⊢ x = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to (\{x, y\} \notin E \leftrightarrow \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E)$
148	147	ralbidv	$⊢ x = ⟨1, (2^{nd} (X) - K) \mod N⟩ \to (\forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E)$
149	71 72 73 140 144 148	raltp	$⊢ \forall x \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{x, y\} \notin E \leftrightarrow (\forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) + K) \mod N⟩, y\} \notin E \land \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨0, 2^{nd} (X)⟩, y\} \notin E \land \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{⟨1, (2^{nd} (X) - K) \mod N⟩, y\} \notin E)$
150	84 109 136 149	syl3anbrc	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \forall x \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{x, y\} \notin E$
151	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⟩\}$
152	8 151	sylanl1	$⊢ ((N = 5 \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⟩\}$
153	152	raleqdv	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\forall y \in U \{x, y\} \notin E \leftrightarrow \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{x, y\} \notin E)$
154	152 153	raleqbidv	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\forall x \in U \forall y \in U \{x, y\} \notin E \leftrightarrow \forall x \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \forall y \in \{⟨1, (2^{nd} (X) + K) \mod N⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \{x, y\} \notin E)$
155	150 154	mpbird	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to \forall x \in U \forall y \in U \{x, y\} \notin E$
156	46 155	jca	$⊢ ((N = 5 \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)$
157	156	exp43	$⊢ N = 5 \to (K \in J \to (X \in V \to (1^{st} (X) = 1 \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))))$
158	157	3imp	$⊢ (N = 5 \land K \in J \land X \in V) \to (1^{st} (X) = 1 \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
159	44 158	syl5	$⊢ (N = 5 \land K \in J \land X \in V) \to (X = ⟨1, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
160	159	adantl	$⊢ (a = 1 \land (N = 5 \land K \in J \land X \in V)) \to (X = ⟨1, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
161	42 160	sylbid	$⊢ (a = 1 \land (N = 5 \land K \in J \land X \in V)) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
162	161	ex	$⊢ a = 1 \to ((N = 5 \land K \in J \land X \in V) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)))$
163	39 162	jaoi	$⊢ (a = 0 \lor a = 1) \to ((N = 5 \land K \in J \land X \in V) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)))$
164	14 163	syl	$⊢ a \in \{0, 1\} \to ((N = 5 \land K \in J \land X \in V) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)))$
165	164	impcom	$⊢ ((N = 5 \land K \in J \land X \in V) \land a \in \{0, 1\}) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
166	165	a1d	$⊢ ((N = 5 \land K \in J \land X \in V) \land a \in \{0, 1\}) \to (b \in (0 ..^N) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)))$
167	166	expimpd	$⊢ (N = 5 \land K \in J \land X \in V) \to ((a \in \{0, 1\} \land b \in (0 ..^N)) \to (X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)))$
168	167	rexlimdvv	$⊢ (N = 5 \land K \in J \land X \in V) \to (\exists a \in \{0, 1\} \exists b \in (0 ..^N) X = ⟨a, b⟩ \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E))$
169	13 168	mpd	$⊢ (N = 5 \land K \in J \land X \in V) \to (\|U\| = 3 \land \forall x \in U \forall y \in U \{x, y\} \notin E)$

Metamath Proof Explorer

Theorem gpg5nbgr3star

Proof