gpg5nbgrvtx13starlem3

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

Metamath Proof Explorer

Theorem gpg5nbgrvtx13starlem3

Proof