gpg5nbgrvtx13starlem1

	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	gpg5nbgrvtx13starlem1	$⊢ ((N = 5 \land K \in J) \land X \in W) \to \{⟨1, (X + K) \mod N⟩, ⟨0, 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	$⊢ ⟨1, (X + K) \mod N⟩ \in V$
6		opex	$⊢ ⟨0, X⟩ \in V$
7	5 6	pm3.2i	$⊢ (⟨1, (X + K) \mod N⟩ \in V \land ⟨0, 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	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨0, 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 + K) \mod N \neq x)$
14		1ex	$⊢ 1 \in V$
15		ovex	$⊢ (X + K) \mod N \in V$
16	14 15	opthne	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (1 \neq 0 \lor (X + K) \mod N \neq x)$
17	13 16	mpbir	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩$
18	12	orci	$⊢ (1 \neq 0 \lor (X + K) \mod N \neq (x + 1) \mod N)$
19	14 15	opthne	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (1 \neq 0 \lor (X + K) \mod N \neq (x + 1) \mod N)$
20	18 19	mpbir	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩$
21	17 20	pm3.2i	$⊢ (⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \land ⟨1, (X + K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩)$
22	21	a1i	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \land ⟨1, (X + K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩)$
23	22	orcd	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ((⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \land ⟨1, (X + K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩) \lor (⟨0, X⟩ \neq ⟨0, x⟩ \land ⟨0, X⟩ \neq ⟨0, (x + 1) \mod N⟩))$
24		prneimg	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨0, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V)) \to (((⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \land ⟨1, (X + K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩) \lor (⟨0, X⟩ \neq ⟨0, x⟩ \land ⟨0, X⟩ \neq ⟨0, (x + 1) \mod N⟩)) \to \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\})$
25	11 23 24	mpsyl	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
26		0ne1	$⊢ 0 \neq 1$
27	26	orci	$⊢ (0 \neq 1 \lor X \neq x)$
28		c0ex	$⊢ 0 \in V$
29	28	a1i	$⊢ (N = 5 \land K \in J) \to 0 \in V$
30	29	anim1i	$⊢ ((N = 5 \land K \in J) \land X \in W) \to (0 \in V \land X \in W)$
31	30	adantr	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (0 \in V \land X \in W)$
32		opthneg	$⊢ (0 \in V \land X \in W) \to (⟨0, X⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor X \neq x))$
33	31 32	syl	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨0, X⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor X \neq x))$
34	27 33	mpbiri	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ⟨0, X⟩ \neq ⟨1, x⟩$
35	34	olcd	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, X⟩ \neq ⟨1, x⟩)$
36		eleq1	$⊢ X = x \to (X \in (0 ..^N) \leftrightarrow x \in (0 ..^N))$
37	36	adantr	$⊢ (X = x \land ((N = 5 \land K \in J) \land X \in W)) \to (X \in (0 ..^N) \leftrightarrow x \in (0 ..^N))$
38		oveq2	$⊢ N = 5 \to (0 ..^N) = (0 ..^5)$
39	38	eleq2d	$⊢ N = 5 \to (X \in (0 ..^N) \leftrightarrow X \in (0 ..^5))$
40	39	biimpd	$⊢ N = 5 \to (X \in (0 ..^N) \to X \in (0 ..^5))$
41	40	ad2antrr	$⊢ ((N = 5 \land K \in J) \land X \in W) \to (X \in (0 ..^N) \to X \in (0 ..^5))$
42	41	imp	$⊢ (((N = 5 \land K \in J) \land X \in W) \land X \in (0 ..^N)) \to X \in (0 ..^5)$
43		5nn	$⊢ 5 \in ℕ$
44		eleq1	$⊢ N = 5 \to (N \in ℕ \leftrightarrow 5 \in ℕ)$
45	43 44	mpbiri	$⊢ N = 5 \to N \in ℕ$
46	1	ceilhalfelfzo1	$⊢ N \in ℕ \to (K \in J \to K \in (1 ..^N))$
47	45 46	syl	$⊢ N = 5 \to (K \in J \to K \in (1 ..^N))$
48		oveq2	$⊢ N = 5 \to (1 ..^N) = (1 ..^5)$
49	48	eleq2d	$⊢ N = 5 \to (K \in (1 ..^N) \leftrightarrow K \in (1 ..^5))$
50	47 49	sylibd	$⊢ N = 5 \to (K \in J \to K \in (1 ..^5))$
51	50	imp	$⊢ (N = 5 \land K \in J) \to K \in (1 ..^5)$
52	51	ad2antrr	$⊢ (((N = 5 \land K \in J) \land X \in W) \land X \in (0 ..^N)) \to K \in (1 ..^5)$
53		plusmod5ne	$⊢ (X \in (0 ..^5) \land K \in (1 ..^5)) \to (X + K) \mod 5 \neq X$
54	42 52 53	syl2anc	$⊢ (((N = 5 \land K \in J) \land X \in W) \land X \in (0 ..^N)) \to (X + K) \mod 5 \neq X$
55		oveq2	$⊢ N = 5 \to (X + K) \mod N = (X + K) \mod 5$
56	55	neeq1d	$⊢ N = 5 \to ((X + K) \mod N \neq X \leftrightarrow (X + K) \mod 5 \neq X)$
57	56	adantr	$⊢ (N = 5 \land K \in J) \to ((X + K) \mod N \neq X \leftrightarrow (X + K) \mod 5 \neq X)$
58	57	ad2antrr	$⊢ (((N = 5 \land K \in J) \land X \in W) \land X \in (0 ..^N)) \to ((X + K) \mod N \neq X \leftrightarrow (X + K) \mod 5 \neq X)$
59	54 58	mpbird	$⊢ (((N = 5 \land K \in J) \land X \in W) \land X \in (0 ..^N)) \to (X + K) \mod N \neq X$
60	59	ex	$⊢ ((N = 5 \land K \in J) \land X \in W) \to (X \in (0 ..^N) \to (X + K) \mod N \neq X)$
61	60	adantl	$⊢ (X = x \land ((N = 5 \land K \in J) \land X \in W)) \to (X \in (0 ..^N) \to (X + K) \mod N \neq X)$
62	37 61	sylbird	$⊢ (X = x \land ((N = 5 \land K \in J) \land X \in W)) \to (x \in (0 ..^N) \to (X + K) \mod N \neq X)$
63	62	impr	$⊢ (X = x \land (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N))) \to (X + K) \mod N \neq X$
64		neeq2	$⊢ X = x \to ((X + K) \mod N \neq X \leftrightarrow (X + K) \mod N \neq x)$
65	64	adantr	$⊢ (X = x \land (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N))) \to ((X + K) \mod N \neq X \leftrightarrow (X + K) \mod N \neq x)$
66	63 65	mpbid	$⊢ (X = x \land (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N))) \to (X + K) \mod N \neq x$
67	66	orcd	$⊢ (X = x \land (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N))) \to ((X + K) \mod N \neq x \lor X \neq x)$
68	67	ex	$⊢ X = x \to ((((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq x \lor X \neq x))$
69		olc	$⊢ X \neq x \to ((X + K) \mod N \neq x \lor X \neq x)$
70	69	a1d	$⊢ X \neq x \to ((((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq x \lor X \neq x))$
71	68 70	pm2.61ine	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq x \lor X \neq x)$
72	14 15	opthne	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (1 \neq 1 \lor (X + K) \mod N \neq x)$
73		neirr	$⊢ \neg 1 \neq 1$
74	73	biorfi	$⊢ (X + K) \mod N \neq x \leftrightarrow (1 \neq 1 \lor (X + K) \mod N \neq x)$
75	72 74	bitr4i	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (X + K) \mod N \neq x$
76	75	a1i	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (X + K) \mod N \neq x)$
77		opthneg	$⊢ (0 \in V \land X \in W) \to (⟨0, X⟩ \neq ⟨0, x⟩ \leftrightarrow (0 \neq 0 \lor X \neq x))$
78	31 77	syl	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨0, X⟩ \neq ⟨0, x⟩ \leftrightarrow (0 \neq 0 \lor X \neq x))$
79		neirr	$⊢ \neg 0 \neq 0$
80	79	biorfi	$⊢ X \neq x \leftrightarrow (0 \neq 0 \lor X \neq x)$
81	78 80	bitr4di	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨0, X⟩ \neq ⟨0, x⟩ \leftrightarrow X \neq x)$
82	76 81	orbi12d	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ((⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, X⟩ \neq ⟨0, x⟩) \leftrightarrow ((X + K) \mod N \neq x \lor X \neq x))$
83	71 82	mpbird	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, X⟩ \neq ⟨0, x⟩)$
84	35 83	jca	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ((⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, X⟩ \neq ⟨1, x⟩) \land (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, X⟩ \neq ⟨0, x⟩))$
85		opex	$⊢ ⟨1, x⟩ \in V$
86	8 85	pm3.2i	$⊢ (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)$
87	7 86	pm3.2i	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨0, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V))$
88		prneimg2	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨0, X⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)) \to (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, X⟩ \neq ⟨1, x⟩) \land (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, X⟩ \neq ⟨0, x⟩)))$
89	87 88	mp1i	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨0, X⟩ \neq ⟨1, x⟩) \land (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨0, X⟩ \neq ⟨0, x⟩)))$
90	84 89	mpbird	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\}$
91		opex	$⊢ ⟨1, (x + K) \mod N⟩ \in V$
92	85 91	pm3.2i	$⊢ (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)$
93	7 92	pm3.2i	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨0, X⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V))$
94	26	a1i	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to 0 \neq 1$
95	94	orcd	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (0 \neq 1 \lor X \neq (x + K) \mod N)$
96		opthneg	$⊢ (0 \in V \land X \in W) \to (⟨0, X⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (0 \neq 1 \lor X \neq (x + K) \mod N))$
97	31 96	syl	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨0, X⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (0 \neq 1 \lor X \neq (x + K) \mod N))$
98	95 97	mpbird	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ⟨0, X⟩ \neq ⟨1, (x + K) \mod N⟩$
99	34 98	jca	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (⟨0, X⟩ \neq ⟨1, x⟩ \land ⟨0, X⟩ \neq ⟨1, (x + K) \mod N⟩)$
100	99	olcd	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to ((⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \land ⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩) \lor (⟨0, X⟩ \neq ⟨1, x⟩ \land ⟨0, X⟩ \neq ⟨1, (x + K) \mod N⟩))$
101		prneimg	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨0, X⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)) \to (((⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \land ⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩) \lor (⟨0, X⟩ \neq ⟨1, x⟩ \land ⟨0, X⟩ \neq ⟨1, (x + K) \mod N⟩)) \to \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
102	93 100 101	mpsyl	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
103	25 90 102	3jca	$⊢ (((N = 5 \land K \in J) \land X \in W) \land x \in (0 ..^N)) \to (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
104	103	ralrimiva	$⊢ ((N = 5 \land K \in J) \land X \in W) \to \forall x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
105		ralnex	$⊢ \forall x \in (0 ..^N) \neg (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \neg \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
106		3ioran	$⊢ \neg (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
107		df-ne	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
108		df-ne	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\}$
109		df-ne	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
110	107 108 109	3anbi123i	$⊢ (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
111	106 110	bitr4i	$⊢ \neg (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
112	111	ralbii	$⊢ \forall x \in (0 ..^N) \neg (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
113	105 112	bitr3i	$⊢ \neg \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
114	104 113	sylibr	$⊢ ((N = 5 \land K \in J) \land X \in W) \to \neg \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
115		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
116		eleq1	$⊢ N = 5 \to (N \in ℤ_{\geq 3} \leftrightarrow 5 \in ℤ_{\geq 3})$
117	115 116	mpbiri	$⊢ N = 5 \to N \in ℤ_{\geq 3}$
118		eqid	$⊢ (0 ..^N) = (0 ..^N)$
119	118 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
120	117 119	sylan	$⊢ (N = 5 \land K \in J) \to (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
121	120	adantr	$⊢ ((N = 5 \land K \in J) \land X \in W) \to (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
122	114 121	mtbird	$⊢ ((N = 5 \land K \in J) \land X \in W) \to \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \in E$
123		df-nel	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \notin E \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \in E$
124	122 123	sylibr	$⊢ ((N = 5 \land K \in J) \land X \in W) \to \{⟨1, (X + K) \mod N⟩, ⟨0, X⟩\} \notin E$

Metamath Proof Explorer

Theorem gpg5nbgrvtx13starlem1

Proof