gpg5nbgrvtx03starlem2

Description: Lemma 2 for gpg5nbgrvtx03star . (Contributed by AV, 6-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	gpg5nbgrvtx03starlem2	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to \{⟨0, (X + 1) \mod N⟩, ⟨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		m1modnep2mod	$⊢ (N \in ℤ_{\geq 4} \land X \in ℤ) \to (X - 1) \mod N \neq (X + 2) \mod N$
6	5	3adant2	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X - 1) \mod N \neq (X + 2) \mod N$
7		zcn	$⊢ X \in ℤ \to X \in ℂ$
8	7	3ad2ant3	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to X \in ℂ$
9		add1p1	$⊢ X \in ℂ \to X + 1 + 1 = X + 2$
10	8 9	syl	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to X + 1 + 1 = X + 2$
11	10	oveq1d	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X + 1 + 1) \mod N = (X + 2) \mod N$
12	6 11	neeqtrrd	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X - 1) \mod N \neq (X + 1 + 1) \mod N$
13		zre	$⊢ X \in ℤ \to X \in ℝ$
14	13	3ad2ant3	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to X \in ℝ$
15		1red	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to 1 \in ℝ$
16	14 15	readdcld	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to X + 1 \in ℝ$
17		eluz4nn	$⊢ N \in ℤ_{\geq 4} \to N \in ℕ$
18	17	nnrpd	$⊢ N \in ℤ_{\geq 4} \to N \in ℝ^{+}$
19	18	3ad2ant1	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to N \in ℝ^{+}$
20		modaddmod	$⊢ (X + 1 \in ℝ \land 1 \in ℝ \land N \in ℝ^{+}) \to (((X + 1) \mod N) + 1) \mod N = (X + 1 + 1) \mod N$
21	16 15 19 20	syl3anc	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (((X + 1) \mod N) + 1) \mod N = (X + 1 + 1) \mod N$
22	12 21	neeqtrrd	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X - 1) \mod N \neq (((X + 1) \mod N) + 1) \mod N$
23	22	ad2antrl	$⊢ ((X + 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to (X - 1) \mod N \neq (((X + 1) \mod N) + 1) \mod N$
24		oveq1	$⊢ (X + 1) \mod N = x \to ((X + 1) \mod N) + 1 = x + 1$
25	24	oveq1d	$⊢ (X + 1) \mod N = x \to (((X + 1) \mod N) + 1) \mod N = (x + 1) \mod N$
26	25	adantr	$⊢ ((X + 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to (((X + 1) \mod N) + 1) \mod N = (x + 1) \mod N$
27	23 26	neeqtrd	$⊢ ((X + 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to (X - 1) \mod N \neq (x + 1) \mod N$
28	27	olcd	$⊢ ((X + 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to ((X + 1) \mod N \neq x \lor (X - 1) \mod N \neq (x + 1) \mod N)$
29	28	ex	$⊢ (X + 1) \mod N = x \to (((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq x \lor (X - 1) \mod N \neq (x + 1) \mod N))$
30		orc	$⊢ (X + 1) \mod N \neq x \to ((X + 1) \mod N \neq x \lor (X - 1) \mod N \neq (x + 1) \mod N)$
31	30	a1d	$⊢ (X + 1) \mod N \neq x \to (((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq x \lor (X - 1) \mod N \neq (x + 1) \mod N))$
32	29 31	pm2.61ine	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq x \lor (X - 1) \mod N \neq (x + 1) \mod N)$
33		c0ex	$⊢ 0 \in V$
34		ovex	$⊢ (X + 1) \mod N \in V$
35	33 34	opthne	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (0 \neq 0 \lor (X + 1) \mod N \neq x)$
36		neirr	$⊢ \neg 0 \neq 0$
37	36	biorfi	$⊢ (X + 1) \mod N \neq x \leftrightarrow (0 \neq 0 \lor (X + 1) \mod N \neq x)$
38	35 37	bitr4i	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (X + 1) \mod N \neq x$
39	38	a1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (X + 1) \mod N \neq x)$
40		ovex	$⊢ (X - 1) \mod N \in V$
41	33 40	opthne	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (0 \neq 0 \lor (X - 1) \mod N \neq (x + 1) \mod N)$
42	36	biorfi	$⊢ (X - 1) \mod N \neq (x + 1) \mod N \leftrightarrow (0 \neq 0 \lor (X - 1) \mod N \neq (x + 1) \mod N)$
43	41 42	bitr4i	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (X - 1) \mod N \neq (x + 1) \mod N$
44	43	a1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (X - 1) \mod N \neq (x + 1) \mod N)$
45	39 44	orbi12d	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩) \leftrightarrow ((X + 1) \mod N \neq x \lor (X - 1) \mod N \neq (x + 1) \mod N))$
46	32 45	mpbird	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩)$
47		uzuzle24	$⊢ N \in ℤ_{\geq 4} \to N \in ℤ_{\geq 2}$
48	47	anim1i	$⊢ (N \in ℤ_{\geq 4} \land X \in ℤ) \to (N \in ℤ_{\geq 2} \land X \in ℤ)$
49	48	3adant2	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (N \in ℤ_{\geq 2} \land X \in ℤ)$
50		zp1modne	$⊢ (N \in ℤ_{\geq 2} \land X \in ℤ) \to (X + 1) \mod N \neq X \mod N$
51	49 50	syl	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X + 1) \mod N \neq X \mod N$
52		npcan1	$⊢ X \in ℂ \to X - 1 + 1 = X$
53	8 52	syl	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to X - 1 + 1 = X$
54	53	oveq1d	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X - 1 + 1) \mod N = X \mod N$
55	51 54	neeqtrrd	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X + 1) \mod N \neq (X - 1 + 1) \mod N$
56	14 15	resubcld	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to X - 1 \in ℝ$
57		modaddmod	$⊢ (X - 1 \in ℝ \land 1 \in ℝ \land N \in ℝ^{+}) \to (((X - 1) \mod N) + 1) \mod N = (X - 1 + 1) \mod N$
58	56 15 19 57	syl3anc	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (((X - 1) \mod N) + 1) \mod N = (X - 1 + 1) \mod N$
59	55 58	neeqtrrd	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (X + 1) \mod N \neq (((X - 1) \mod N) + 1) \mod N$
60	59	ad2antrl	$⊢ ((X - 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to (X + 1) \mod N \neq (((X - 1) \mod N) + 1) \mod N$
61		oveq1	$⊢ (X - 1) \mod N = x \to ((X - 1) \mod N) + 1 = x + 1$
62	61	oveq1d	$⊢ (X - 1) \mod N = x \to (((X - 1) \mod N) + 1) \mod N = (x + 1) \mod N$
63	62	adantr	$⊢ ((X - 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to (((X - 1) \mod N) + 1) \mod N = (x + 1) \mod N$
64	60 63	neeqtrd	$⊢ ((X - 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to (X + 1) \mod N \neq (x + 1) \mod N$
65	64	orcd	$⊢ ((X - 1) \mod N = x \land ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N))) \to ((X + 1) \mod N \neq (x + 1) \mod N \lor (X - 1) \mod N \neq x)$
66	65	ex	$⊢ (X - 1) \mod N = x \to (((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq (x + 1) \mod N \lor (X - 1) \mod N \neq x))$
67		olc	$⊢ (X - 1) \mod N \neq x \to ((X + 1) \mod N \neq (x + 1) \mod N \lor (X - 1) \mod N \neq x)$
68	67	a1d	$⊢ (X - 1) \mod N \neq x \to (((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq (x + 1) \mod N \lor (X - 1) \mod N \neq x))$
69	66 68	pm2.61ine	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + 1) \mod N \neq (x + 1) \mod N \lor (X - 1) \mod N \neq x)$
70	33 34	opthne	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (0 \neq 0 \lor (X + 1) \mod N \neq (x + 1) \mod N)$
71	36	biorfi	$⊢ (X + 1) \mod N \neq (x + 1) \mod N \leftrightarrow (0 \neq 0 \lor (X + 1) \mod N \neq (x + 1) \mod N)$
72	70 71	bitr4i	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (X + 1) \mod N \neq (x + 1) \mod N$
73	72	a1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (X + 1) \mod N \neq (x + 1) \mod N)$
74	33 40	opthne	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (0 \neq 0 \lor (X - 1) \mod N \neq x)$
75	36	biorfi	$⊢ (X - 1) \mod N \neq x \leftrightarrow (0 \neq 0 \lor (X - 1) \mod N \neq x)$
76	74 75	bitr4i	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (X - 1) \mod N \neq x$
77	76	a1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (X - 1) \mod N \neq x)$
78	73 77	orbi12d	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩) \leftrightarrow ((X + 1) \mod N \neq (x + 1) \mod N \lor (X - 1) \mod N \neq x))$
79	69 78	mpbird	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩)$
80		opex	$⊢ ⟨0, (X + 1) \mod N⟩ \in V$
81		opex	$⊢ ⟨0, (X - 1) \mod N⟩ \in V$
82	80 81	pm3.2i	$⊢ (⟨0, (X + 1) \mod N⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V)$
83		opex	$⊢ ⟨0, x⟩ \in V$
84		opex	$⊢ ⟨0, (x + 1) \mod N⟩ \in V$
85	83 84	pm3.2i	$⊢ (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V)$
86	82 85	pm3.2i	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V))$
87		prneimg2	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩)))$
88	86 87	mp1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩)))$
89	46 79 88	mpbir2and	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
90		0ne1	$⊢ 0 \neq 1$
91	90	orci	$⊢ (0 \neq 1 \lor (X - 1) \mod N \neq x)$
92	33 40	opthne	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor (X - 1) \mod N \neq x)$
93	91 92	mpbir	$⊢ ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩$
94	93	olci	$⊢ (⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩)$
95	90	orci	$⊢ (0 \neq 1 \lor (X + 1) \mod N \neq x)$
96	33 34	opthne	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor (X + 1) \mod N \neq x)$
97	95 96	mpbir	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩$
98	97	orci	$⊢ (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩)$
99	94 98	pm3.2i	$⊢ ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩))$
100	99	a1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩))$
101		opex	$⊢ ⟨1, x⟩ \in V$
102	83 101	pm3.2i	$⊢ (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)$
103	82 102	pm3.2i	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V))$
104		prneimg2	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩)))$
105	103 104	mp1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨0, (X + 1) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩) \land (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, (X - 1) \mod N⟩ \neq ⟨0, x⟩)))$
106	100 105	mpbird	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\}$
107		opex	$⊢ ⟨1, (x + K) \mod N⟩ \in V$
108	101 107	pm3.2i	$⊢ (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)$
109	82 108	pm3.2i	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V))$
110	90	orci	$⊢ (0 \neq 1 \lor (X + 1) \mod N \neq (x + K) \mod N)$
111	33 34	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)$
112	110 111	mpbir	$⊢ ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩$
113	97 112	pm3.2i	$⊢ (⟨0, (X + 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X + 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩)$
114	113	a1i	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \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⟩)$
115	114	orcd	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \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 (⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X - 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩))$
116		prneimg	$⊢ ((⟨0, (X + 1) \mod N⟩ \in V \land ⟨0, (X - 1) \mod N⟩ \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 (⟨0, (X - 1) \mod N⟩ \neq ⟨1, x⟩ \land ⟨0, (X - 1) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩)) \to \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
117	109 115 116	mpsyl	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
118	89 106 117	3jca	$⊢ ((N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \land x \in (0 ..^N)) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
119	118	ralrimiva	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to \forall x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
120		ralnex	$⊢ \forall x \in (0 ..^N) \neg (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \neg \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
121		3ioran	$⊢ \neg (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
122		df-ne	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
123		df-ne	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\}$
124		df-ne	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
125	122 123 124	3anbi123i	$⊢ (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
126	121 125	bitr4i	$⊢ \neg (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
127	126	ralbii	$⊢ \forall x \in (0 ..^N) \neg (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
128	120 127	bitr3i	$⊢ \neg \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
129	119 128	sylibr	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to \neg \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
130		uzuzle34	$⊢ N \in ℤ_{\geq 4} \to N \in ℤ_{\geq 3}$
131		eqid	$⊢ (0 ..^N) = (0 ..^N)$
132	131 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
133	130 132	sylan	$⊢ (N \in ℤ_{\geq 4} \land K \in J) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
134	133	3adant3	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
135	129 134	mtbird	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \in E$
136		df-nel	$⊢ \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \notin E \leftrightarrow \neg \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \in E$
137	135 136	sylibr	$⊢ (N \in ℤ_{\geq 4} \land K \in J \land X \in ℤ) \to \{⟨0, (X + 1) \mod N⟩, ⟨0, (X - 1) \mod N⟩\} \notin E$

Metamath Proof Explorer

Theorem gpg5nbgrvtx03starlem2

Proof