gpg5nbgrvtx03starlem3

Description: Lemma 3 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	gpg5nbgrvtx03starlem3	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \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	$⊢ ⟨1, X⟩ \in V$
6		opex	$⊢ ⟨0, (X - 1) \mod N⟩ \in V$
7	5 6	pm3.2i	$⊢ (⟨1, X⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \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	$⊢ ((⟨1, X⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V))$
12		ax-1ne0	$⊢ 1 \neq 0$
13	12	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to 1 \neq 0$
14	13	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)$
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	orci	$⊢ (1 \neq 0 \lor X \neq (x + 1) \mod N)$
24	23	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 + 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	orcd	$⊢ ((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⟩) \lor (⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩ \land ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩))$
30		prneimg	$⊢ ((⟨1, X⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V)) \to (((⟨1, X⟩ \neq ⟨0, x⟩ \land ⟨1, X⟩ \neq ⟨0, (x + 1) \mod N⟩) \lor (⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩ \land ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩)) \to \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \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 \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \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		m1modne	$⊢ (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	6 5	pm3.2i	$⊢ (⟨0, (X - 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V)$
67		opex	$⊢ ⟨1, x⟩ \in V$
68	8 67	pm3.2i	$⊢ (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)$
69	66 68	pm3.2i	$⊢ ((⟨0, (X - 1) \mod N⟩ \in V \land ⟨1, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V))$
70		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⟩)))$
71	69 70	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⟩)))$
72	65 71	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⟩\}$
73		prcom	$⊢ \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, (X - 1) \mod N⟩, ⟨1, X⟩\}$
74	73	neeq1i	$⊢ \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow \{⟨0, (X - 1) \mod N⟩, ⟨1, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\}$
75	72 74	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\}$
76		opex	$⊢ ⟨1, (x + K) \mod N⟩ \in V$
77	67 76	pm3.2i	$⊢ (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)$
78	7 77	pm3.2i	$⊢ ((⟨1, X⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V))$
79		0ne1	$⊢ 0 \neq 1$
80	79	orci	$⊢ (0 \neq 1 \lor (X - 1) \mod N \neq x)$
81	50 51	opthne	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor (X - 1) \mod N \neq x)$
82	80 81	mpbir	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩$
83	79	orci	$⊢ (0 \neq 1 \lor (X - 1) \mod N \neq (x + K) \mod N)$
84	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)$
85	83 84	mpbir	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩$
86	82 85	pm3.2i	$⊢ (⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X - 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩)$
87	86	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⟩)$
88	87	olcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to ((⟨1, X⟩ \neq ⟨1, x⟩ \land ⟨1, X⟩ \neq ⟨1, (x + K) \mod N⟩) \lor (⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X - 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩))$
89		prneimg	$⊢ ((⟨1, X⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)) \to (((⟨1, X⟩ \neq ⟨1, x⟩ \land ⟨1, X⟩ \neq ⟨1, (x + K) \mod N⟩) \lor (⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X - 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩)) \to \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
90	78 88 89	mpsyl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
91	31 75 90	3jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J \land X \in W) \land x \in (0 ..^N)) \to (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
92	91	ralrimiva	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \forall x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
93		ralnex	$⊢ \forall x \in (0 ..^N) \neg (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \neg \exists x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
94		3ioran	$⊢ \neg (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
95		df-ne	$⊢ \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
96		df-ne	$⊢ \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\}$
97		df-ne	$⊢ \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
98	95 96 97	3anbi123i	$⊢ (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
99	94 98	bitr4i	$⊢ \neg (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
100	99	ralbii	$⊢ \forall x \in (0 ..^N) \neg (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
101	93 100	bitr3i	$⊢ \neg \exists x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
102	92 101	sylibr	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \neg \exists x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
103		eqid	$⊢ (0 ..^N) = (0 ..^N)$
104	103 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
105	104	3adant3	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
106	102 105	mtbird	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \in E$
107		df-nel	$⊢ \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \notin E \leftrightarrow \neg \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \in E$
108	106 107	sylibr	$⊢ (N \in ℤ_{\geq 3} \land K \in J \land X \in W) \to \{⟨1, X⟩, ⟨0, (X - 1) \mod N⟩\} \notin E$

Metamath Proof Explorer

Theorem gpg5nbgrvtx03starlem3

Proof