gpg5nbgrvtx03starlem1

Description: Lemma 1 for gpg5nbgrvtx03star . (Contributed by AV, 5-Sep-2025)

	Ref	Expression
Hypotheses	gpg5nbgrvtx03starlem1.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpg5nbgrvtx03starlem1.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpg5nbgrvtx03starlem1.v	$⊢ V = Vtx (G)$
	gpg5nbgrvtx03starlem1.e	$⊢ E = Edg (G)$
Assertion	gpg5nbgrvtx03starlem1	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \notin E$

Proof

Step	Hyp	Ref	Expression
1		gpg5nbgrvtx03starlem1.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpg5nbgrvtx03starlem1.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
3		gpg5nbgrvtx03starlem1.v	$⊢ V = Vtx (G)$
4		gpg5nbgrvtx03starlem1.e	$⊢ E = Edg (G)$
5		opex	$⊢ ⟨0, (X + 1) \mod N⟩ \in V$
6		opex	$⊢ ⟨1, X⟩ \in V$
7	5 6	pm3.2i	$⊢ (⟨0, (X + 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V)$
8		opex	$⊢ ⟨0, x⟩ \in V$
9		opex	$⊢ ⟨0, (x + 1) \mod N⟩ \in V$
10	8 9	pm3.2i	$⊢ (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V)$
11	7 10	pm3.2i	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V))$
12		ax-1ne0	$⊢ 1 \neq 0$
13	12	orci	$⊢ (1 \neq 0 \lor X \neq x)$
14	13	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (1 \neq 0 \lor X \neq x)$
15		1ex	$⊢ 1 \in V$
16	15	a1i	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to 1 \in V$
17		simp3	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to X \in W$
18	16 17	jca	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to (1 \in V \land X \in W)$
19	18	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (1 \in V \land X \in W)$
20		opthneg	$⊢ (1 \in V \land X \in W) \to (⟨1, X⟩ \neq ⟨0, x⟩ \leftrightarrow (1 \neq 0 \lor X \neq x))$
21	19 20	syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨1, X⟩ \neq ⟨0, x⟩ \leftrightarrow (1 \neq 0 \lor X \neq x))$
22	14 21	mpbird	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ⟨1, X⟩ \neq ⟨0, x⟩$
23	12	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to 1 \neq 0$
24	23	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (1 \neq 0 \lor X \neq (x + 1) \mod N)$
25		opthneg	$⊢ (1 \in V \land X \in W) \to (⟨1, X⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (1 \neq 0 \lor X \neq (x + 1) \mod N))$
26	19 25	syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨1, X⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (1 \neq 0 \lor X \neq (x + 1) \mod N))$
27	24 26	mpbird	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ⟨1, X⟩ \neq ⟨0, (x + 1) \mod N⟩$
28	22 27	jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨1, X⟩ \neq ⟨0, x⟩ \land ⟨1, X⟩ \neq ⟨0, (x + 1) \mod N⟩)$
29	28	olcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \land ⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩) \lor (⟨1, X⟩ \neq ⟨0, x⟩ \land ⟨1, X⟩ \neq ⟨0, (x + 1) \mod N⟩))$
30		prneimg	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V)) \to (((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \land ⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩) \lor (⟨1, X⟩ \neq ⟨0, x⟩ \land ⟨1, X⟩ \neq ⟨0, (x + 1) \mod N⟩)) \to \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\})$
31	11 29 30	mpsyl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
32		eleq1	$⊢ X = x \to (X \in (0 ..^N) \leftrightarrow x \in (0 ..^N))$
33	32	adantr	$⊢ (X = x \land (N \in ℤ_{\geq 3} \land K \in J \land X \in W)) \to (X \in (0 ..^N) \leftrightarrow x \in (0 ..^N))$
34		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
35	34	3ad2ant1	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to N \in ℤ_{\geq 2}$
36		p1modne	$⊢ (N \in ℤ_{\geq 2} \land X \in (0 ..^N)) \to (X + 1) \mod N \neq X$
37	35 36	sylan	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land X \in (0 ..^N)) \to (X + 1) \mod N \neq X$
38	37	ex	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to (X \in (0 ..^N) \to (X + 1) \mod N \neq X)$
39	38	adantl	$⊢ (X = x \land (N \in ℤ_{\geq 3} \land K \in J \land X \in W)) \to (X \in (0 ..^N) \to (X + 1) \mod N \neq X)$
40	33 39	sylbird	$⊢ (X = x \land (N \in ℤ_{\geq 3} \land K \in J \land X \in W)) \to (x \in (0 ..^N) \to (X + 1) \mod N \neq X)$
41	40	impr	$⊢ (X = x \land ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N))) \to (X + 1) \mod N \neq X$
42		neeq2	$⊢ X = x \to ((X + 1) \mod N \neq X \leftrightarrow (X + 1) \mod N \neq x)$
43	42	adantr	$⊢ (X = x \land ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N))) \to ((X + 1) \mod N \neq X \leftrightarrow (X + 1) \mod N \neq x)$
44	41 43	mpbid	$⊢ (X = x \land ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N))) \to (X + 1) \mod N \neq x$
45	44	orcd	$⊢ (X = x \land ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N))) \to ((X + 1) \mod N \neq x \lor X \neq x)$
46	45	ex	$⊢ X = x \to (((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq x \lor X \neq x))$
47		olc	$⊢ X \neq x \to ((X + 1) \mod N \neq x \lor X \neq x)$
48	47	a1d	$⊢ X \neq x \to (((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq x \lor X \neq x))$
49	46 48	pm2.61ine	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq x \lor X \neq x)$
50		c0ex	$⊢ 0 \in V$
51		ovex	$⊢ (X + 1) \mod N \in V$
52	50 51	opthne	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (0 \neq 0 \lor (X + 1) \mod N \neq x)$
53		neirr	$⊢ \neg 0 \neq 0$
54	53	biorfi	$⊢ (X + 1) \mod N \neq x \leftrightarrow (0 \neq 0 \lor (X + 1) \mod N \neq x)$
55	52 54	bitr4i	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (X + 1) \mod N \neq x$
56	55	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (X + 1) \mod N \neq x)$
57		opthneg	$⊢ (1 \in V \land X \in W) \to (⟨1, X⟩ \neq ⟨1, x⟩ \leftrightarrow (1 \neq 1 \lor X \neq x))$
58	19 57	syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨1, X⟩ \neq ⟨1, x⟩ \leftrightarrow (1 \neq 1 \lor X \neq x))$
59		neirr	$⊢ \neg 1 \neq 1$
60	59	biorfi	$⊢ X \neq x \leftrightarrow (1 \neq 1 \lor X \neq x)$
61	58 60	bitr4di	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨1, X⟩ \neq ⟨1, x⟩ \leftrightarrow X \neq x)$
62	56 61	orbi12d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, X⟩ \neq ⟨1, x⟩) \leftrightarrow ((X + 1) \mod N \neq x \lor X \neq x))$
63	49 62	mpbird	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, X⟩ \neq ⟨1, x⟩)$
64	22	olcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, X⟩ \neq ⟨0, x⟩)$
65	63 64	jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, X⟩ \neq ⟨1, x⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, X⟩ \neq ⟨0, x⟩))$
66		opex	$⊢ ⟨1, x⟩ \in V$
67	8 66	pm3.2i	$⊢ (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)$
68	7 67	pm3.2i	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V))$
69		prneimg2	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, X⟩ \neq ⟨1, x⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, X⟩ \neq ⟨0, x⟩)))$
70	68 69	mp1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, X⟩ \neq ⟨1, x⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, X⟩ \neq ⟨0, x⟩)))$
71	65 70	mpbird	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\}$
72		opex	$⊢ ⟨1, (x + K) \mod N⟩ \in V$
73	66 72	pm3.2i	$⊢ (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)$
74	7 73	pm3.2i	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V))$
75		0ne1	$⊢ 0 \neq 1$
76	75	orci	$⊢ (0 \neq 1 \lor (X + 1) \mod N \neq x)$
77	50 51	opthne	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor (X + 1) \mod N \neq x)$
78	76 77	mpbir	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩$
79	75	orci	$⊢ (0 \neq 1 \lor (X + 1) \mod N \neq (x + K) \mod N)$
80	50 51	opthne	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (0 \neq 1 \lor (X + 1) \mod N \neq (x + K) \mod N)$
81	79 80	mpbir	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩$
82	78 81	pm3.2i	$⊢ (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩)$
83	82	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩)$
84	83	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩) \lor (⟨1, X⟩ \neq ⟨1, x⟩ \land ⟨1, X⟩ \neq ⟨1, (x + K) \mod N⟩))$
85		prneimg	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)) \to (((⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩) \lor (⟨1, X⟩ \neq ⟨1, x⟩ \land ⟨1, X⟩ \neq ⟨1, (x + K) \mod N⟩)) \to \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
86	74 84 85	mpsyl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
87	31 71 86	3jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
88	87	ralrimiva	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \forall x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
89		ralnex	$⊢ \forall x \in (0 ..^N) \neg (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \neg \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
90		3ioran	$⊢ \neg (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
91		df-ne	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
92		df-ne	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\}$
93		df-ne	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
94	91 92 93	3anbi123i	$⊢ (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
95	90 94	bitr4i	$⊢ \neg (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
96	95	ralbii	$⊢ \forall x \in (0 ..^N) \neg (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
97	89 96	bitr3i	$⊢ \neg \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
98	88 97	sylibr	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \neg \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
99		eqid	$⊢ (0 ..^N) = (0 ..^N)$
100	99 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
101	100	3adant3	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
102	98 101	mtbird	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \in E$
103		df-nel	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \notin E \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \in E$
104	102 103	sylibr	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \{⟨0, (X + 1) \mod N⟩, ⟨1, X⟩\} \notin E$

Metamath Proof Explorer

Theorem gpg5nbgrvtx03starlem1

Proof