gpg5nbgrvtx13starlem2

	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	gpg5nbgrvtx13starlem2	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to \{⟨1, (X + K) \mod N⟩, ⟨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	$⊢ ⟨1, (X + K) \mod N⟩ \in V$
6		opex	$⊢ ⟨1, (X - K) \mod N⟩ \in V$
7	5 6	pm3.2i	$⊢ (⟨1, (X + K) \mod N⟩ \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	$⊢ ((⟨1, (X + K) \mod N⟩ \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 ℤ) \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 ℤ) \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 (⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩ \land ⟨1, (X - K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩))$
24		prneimg	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨1, (X - K) \mod N⟩ \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 (⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩ \land ⟨1, (X - K) \mod N⟩ \neq ⟨0, (x + 1) \mod N⟩)) \to \{⟨1, (X + K) \mod N⟩, ⟨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 ℤ) \land x \in (0 ..^N)) \to \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
26	17	orci	$⊢ (⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩)$
27	26	a1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩)$
28	12	orci	$⊢ (1 \neq 0 \lor (X - K) \mod N \neq x)$
29		ovex	$⊢ (X - K) \mod N \in V$
30	14 29	opthne	$⊢ ⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩ \leftrightarrow (1 \neq 0 \lor (X - K) \mod N \neq x)$
31	28 30	mpbir	$⊢ ⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩$
32	31	olci	$⊢ (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩)$
33	32	a1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩)$
34		opex	$⊢ ⟨1, x⟩ \in V$
35	8 34	pm3.2i	$⊢ (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)$
36	7 35	pm3.2i	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨1, (X - K) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V))$
37		prneimg2	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨1, (X - K) \mod N⟩ \in V) \land (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V)) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩) \land (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩)))$
38	36 37	mp1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow ((⟨1, (X + K) \mod N⟩ \neq ⟨0, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩) \land (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨0, x⟩)))$
39	27 33 38	mpbir2and	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\}$
40		fvoveq1	$⊢ N = 5 \to ⌈\frac{N}{2}⌉ = ⌈\frac{5}{2}⌉$
41		ceil5half3	$⊢ ⌈\frac{5}{2}⌉ = 3$
42	40 41	eqtrdi	$⊢ N = 5 \to ⌈\frac{N}{2}⌉ = 3$
43	42	oveq2d	$⊢ N = 5 \to (1 ..^⌈\frac{N}{2}⌉) = (1 ..^3)$
44	1 43	eqtrid	$⊢ N = 5 \to J = (1 ..^3)$
45	44	eleq2d	$⊢ N = 5 \to (K \in J \leftrightarrow K \in (1 ..^3))$
46	45	biimpa	$⊢ (N = 5 \land K \in J) \to K \in (1 ..^3)$
47	46	anim1ci	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X \in ℤ \land K \in (1 ..^3))$
48		minusmodnep2tmod	$⊢ (X \in ℤ \land K \in (1 ..^3)) \to (X - K) \mod 5 \neq (X + 2 K) \mod 5$
49	47 48	syl	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X - K) \mod 5 \neq (X + 2 K) \mod 5$
50		oveq2	$⊢ N = 5 \to (X - K) \mod N = (X - K) \mod 5$
51		oveq2	$⊢ N = 5 \to (X + 2 K) \mod N = (X + 2 K) \mod 5$
52	50 51	neeq12d	$⊢ N = 5 \to ((X - K) \mod N \neq (X + 2 K) \mod N \leftrightarrow (X - K) \mod 5 \neq (X + 2 K) \mod 5)$
53	52	ad2antrr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to ((X - K) \mod N \neq (X + 2 K) \mod N \leftrightarrow (X - K) \mod 5 \neq (X + 2 K) \mod 5)$
54	49 53	mpbird	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X - K) \mod N \neq (X + 2 K) \mod N$
55		zcn	$⊢ X \in ℤ \to X \in ℂ$
56	55	adantl	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X \in ℂ$
57		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
58	57 1	eleq2s	$⊢ K \in J \to K \in ℤ$
59	58	zcnd	$⊢ K \in J \to K \in ℂ$
60	59	ad2antlr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to K \in ℂ$
61	56 60 60	addassd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X + K + K = X + K + K$
62	60	2timesd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to 2 K = K + K$
63	62	eqcomd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to K + K = 2 K$
64	63	oveq2d	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X + K + K = X + 2 K$
65	61 64	eqtrd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X + K + K = X + 2 K$
66	65	oveq1d	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X + K + K) \mod N = (X + 2 K) \mod N$
67	54 66	neeqtrrd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X - K) \mod N \neq (X + K + K) \mod N$
68		zre	$⊢ X \in ℤ \to X \in ℝ$
69	68	adantl	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X \in ℝ$
70	58	zred	$⊢ K \in J \to K \in ℝ$
71	70	ad2antlr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to K \in ℝ$
72	69 71	readdcld	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X + K \in ℝ$
73		5nn	$⊢ 5 \in ℕ$
74		eleq1	$⊢ N = 5 \to (N \in ℕ \leftrightarrow 5 \in ℕ)$
75	73 74	mpbiri	$⊢ N = 5 \to N \in ℕ$
76	75	nnrpd	$⊢ N = 5 \to N \in ℝ^{+}$
77	76	ad2antrr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to N \in ℝ^{+}$
78		modaddmod	$⊢ (X + K \in ℝ \land K \in ℝ \land N \in ℝ^{+}) \to (((X + K) \mod N) + K) \mod N = (X + K + K) \mod N$
79	72 71 77 78	syl3anc	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (((X + K) \mod N) + K) \mod N = (X + K + K) \mod N$
80	67 79	neeqtrrd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X - K) \mod N \neq (((X + K) \mod N) + K) \mod N$
81	80	ad2antrl	$⊢ ((X + K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to (X - K) \mod N \neq (((X + K) \mod N) + K) \mod N$
82		oveq1	$⊢ (X + K) \mod N = x \to ((X + K) \mod N) + K = x + K$
83	82	oveq1d	$⊢ (X + K) \mod N = x \to (((X + K) \mod N) + K) \mod N = (x + K) \mod N$
84	83	adantr	$⊢ ((X + K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to (((X + K) \mod N) + K) \mod N = (x + K) \mod N$
85	81 84	neeqtrd	$⊢ ((X + K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to (X - K) \mod N \neq (x + K) \mod N$
86	85	olcd	$⊢ ((X + K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to ((X + K) \mod N \neq x \lor (X - K) \mod N \neq (x + K) \mod N)$
87	86	ex	$⊢ (X + K) \mod N = x \to ((((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq x \lor (X - K) \mod N \neq (x + K) \mod N))$
88		orc	$⊢ (X + K) \mod N \neq x \to ((X + K) \mod N \neq x \lor (X - K) \mod N \neq (x + K) \mod N)$
89	88	a1d	$⊢ (X + K) \mod N \neq x \to ((((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq x \lor (X - K) \mod N \neq (x + K) \mod N))$
90	87 89	pm2.61ine	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq x \lor (X - K) \mod N \neq (x + K) \mod N)$
91	14 15	opthne	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (1 \neq 1 \lor (X + K) \mod N \neq x)$
92		neirr	$⊢ \neg 1 \neq 1$
93	92	biorfi	$⊢ (X + K) \mod N \neq x \leftrightarrow (1 \neq 1 \lor (X + K) \mod N \neq x)$
94	91 93	bitr4i	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (X + K) \mod N \neq x$
95	94	a1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (X + K) \mod N \neq x)$
96	14 29	opthne	$⊢ ⟨1, (X - K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (1 \neq 1 \lor (X - K) \mod N \neq (x + K) \mod N)$
97	92	biorfi	$⊢ (X - K) \mod N \neq (x + K) \mod N \leftrightarrow (1 \neq 1 \lor (X - K) \mod N \neq (x + K) \mod N)$
98	96 97	bitr4i	$⊢ ⟨1, (X - K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (X - K) \mod N \neq (x + K) \mod N$
99	98	a1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X - K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (X - K) \mod N \neq (x + K) \mod N)$
100	95 99	orbi12d	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩) \leftrightarrow ((X + K) \mod N \neq x \lor (X - K) \mod N \neq (x + K) \mod N))$
101	90 100	mpbird	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩)$
102		2z	$⊢ 2 \in ℤ$
103	73	nnzi	$⊢ 5 \in ℤ$
104		2re	$⊢ 2 \in ℝ$
105		5re	$⊢ 5 \in ℝ$
106		2lt5	$⊢ 2 < 5$
107	104 105 106	ltleii	$⊢ 2 \leq 5$
108		eluz2	$⊢ 5 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 5 \in ℤ \land 2 \leq 5)$
109	102 103 107 108	mpbir3an	$⊢ 5 \in ℤ_{\geq 2}$
110		eleq1	$⊢ N = 5 \to (N \in ℤ_{\geq 2} \leftrightarrow 5 \in ℤ_{\geq 2})$
111	109 110	mpbiri	$⊢ N = 5 \to N \in ℤ_{\geq 2}$
112	111	ad2antrr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to N \in ℤ_{\geq 2}$
113		simpr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X \in ℤ$
114	1	ceilhalfelfzo1	$⊢ N \in ℕ \to (K \in J \to K \in (1 ..^N))$
115	75 114	syl	$⊢ N = 5 \to (K \in J \to K \in (1 ..^N))$
116	115	imp	$⊢ (N = 5 \land K \in J) \to K \in (1 ..^N)$
117	116	adantr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to K \in (1 ..^N)$
118		zplusmodne	$⊢ (N \in ℤ_{\geq 2} \land X \in ℤ \land K \in (1 ..^N)) \to (X + K) \mod N \neq X \mod N$
119	112 113 117 118	syl3anc	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X + K) \mod N \neq X \mod N$
120	59	adantl	$⊢ (N = 5 \land K \in J) \to K \in ℂ$
121		npcan	$⊢ (X \in ℂ \land K \in ℂ) \to X - K + K = X$
122	55 120 121	syl2anr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X - K + K = X$
123	122	oveq1d	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X - K + K) \mod N = X \mod N$
124	119 123	neeqtrrd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X + K) \mod N \neq (X - K + K) \mod N$
125	57	zred	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℝ$
126	125 1	eleq2s	$⊢ K \in J \to K \in ℝ$
127	126	ad2antlr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to K \in ℝ$
128	69 127	resubcld	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to X - K \in ℝ$
129		5rp	$⊢ 5 \in ℝ^{+}$
130		eleq1	$⊢ N = 5 \to (N \in ℝ^{+} \leftrightarrow 5 \in ℝ^{+})$
131	129 130	mpbiri	$⊢ N = 5 \to N \in ℝ^{+}$
132	131	ad2antrr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to N \in ℝ^{+}$
133		modaddmod	$⊢ (X - K \in ℝ \land K \in ℝ \land N \in ℝ^{+}) \to (((X - K) \mod N) + K) \mod N = (X - K + K) \mod N$
134	128 127 132 133	syl3anc	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (((X - K) \mod N) + K) \mod N = (X - K + K) \mod N$
135	124 134	neeqtrrd	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (X + K) \mod N \neq (((X - K) \mod N) + K) \mod N$
136	135	ad2antrl	$⊢ ((X - K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to (X + K) \mod N \neq (((X - K) \mod N) + K) \mod N$
137		oveq1	$⊢ (X - K) \mod N = x \to ((X - K) \mod N) + K = x + K$
138	137	oveq1d	$⊢ (X - K) \mod N = x \to (((X - K) \mod N) + K) \mod N = (x + K) \mod N$
139	138	adantr	$⊢ ((X - K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to (((X - K) \mod N) + K) \mod N = (x + K) \mod N$
140	136 139	neeqtrd	$⊢ ((X - K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to (X + K) \mod N \neq (x + K) \mod N$
141	140	orcd	$⊢ ((X - K) \mod N = x \land (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N))) \to ((X + K) \mod N \neq (x + K) \mod N \lor (X - K) \mod N \neq x)$
142	141	ex	$⊢ (X - K) \mod N = x \to ((((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq (x + K) \mod N \lor (X - K) \mod N \neq x))$
143		olc	$⊢ (X - K) \mod N \neq x \to ((X + K) \mod N \neq (x + K) \mod N \lor (X - K) \mod N \neq x)$
144	143	a1d	$⊢ (X - K) \mod N \neq x \to ((((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq (x + K) \mod N \lor (X - K) \mod N \neq x))$
145	142 144	pm2.61ine	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((X + K) \mod N \neq (x + K) \mod N \lor (X - K) \mod N \neq x)$
146	14 15	opthne	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (1 \neq 1 \lor (X + K) \mod N \neq (x + K) \mod N)$
147	92	biorfi	$⊢ (X + K) \mod N \neq (x + K) \mod N \leftrightarrow (1 \neq 1 \lor (X + K) \mod N \neq (x + K) \mod N)$
148	146 147	bitr4i	$⊢ ⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (X + K) \mod N \neq (x + K) \mod N$
149	148	a1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (X + K) \mod N \neq (x + K) \mod N)$
150	14 29	opthne	$⊢ ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (1 \neq 1 \lor (X - K) \mod N \neq x)$
151	92	biorfi	$⊢ (X - K) \mod N \neq x \leftrightarrow (1 \neq 1 \lor (X - K) \mod N \neq x)$
152	150 151	bitr4i	$⊢ ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (X - K) \mod N \neq x$
153	152	a1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩ \leftrightarrow (X - K) \mod N \neq x)$
154	149 153	orbi12d	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to ((⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩) \leftrightarrow ((X + K) \mod N \neq (x + K) \mod N \lor (X - K) \mod N \neq x))$
155	145 154	mpbird	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩)$
156		opex	$⊢ ⟨1, (x + K) \mod N⟩ \in V$
157	34 156	pm3.2i	$⊢ (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)$
158	7 157	pm3.2i	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨1, (X - K) \mod N⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V))$
159		prneimg2	$⊢ ((⟨1, (X + K) \mod N⟩ \in V \land ⟨1, (X - K) \mod N⟩ \in V) \land (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V)) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow ((⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩) \land (⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩)))$
160	158 159	mp1i	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow ((⟨1, (X + K) \mod N⟩ \neq ⟨1, x⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩) \land (⟨1, (X + K) \mod N⟩ \neq ⟨1, (x + K) \mod N⟩ \lor ⟨1, (X - K) \mod N⟩ \neq ⟨1, x⟩)))$
161	101 155 160	mpbir2and	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
162	25 39 161	3jca	$⊢ (((N = 5 \land K \in J) \land X \in ℤ) \land x \in (0 ..^N)) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
163	162	ralrimiva	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to \forall x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
164		ralnex	$⊢ \forall x \in (0 ..^N) \neg (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \neg \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
165		3ioran	$⊢ \neg (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
166		df-ne	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}$
167		df-ne	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\}$
168		df-ne	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}$
169	166 167 168	3anbi123i	$⊢ (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \land \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
170	165 169	bitr4i	$⊢ \neg (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
171	170	ralbii	$⊢ \forall x \in (0 ..^N) \neg (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
172	164 171	bitr3i	$⊢ \neg \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \forall x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨0, x⟩, ⟨1, x⟩\} \land \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \neq \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
173	163 172	sylibr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to \neg \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
174		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
175		eleq1	$⊢ N = 5 \to (N \in ℤ_{\geq 3} \leftrightarrow 5 \in ℤ_{\geq 3})$
176	174 175	mpbiri	$⊢ N = 5 \to N \in ℤ_{\geq 3}$
177		eqid	$⊢ (0 ..^N) = (0 ..^N)$
178	177 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
179	176 178	sylan	$⊢ (N = 5 \land K \in J) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
180	179	adantr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \in E \leftrightarrow \exists x \in (0 ..^N) (\{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
181	173 180	mtbird	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \in E$
182		df-nel	$⊢ \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \notin E \leftrightarrow \neg \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \in E$
183	181 182	sylibr	$⊢ ((N = 5 \land K \in J) \land X \in ℤ) \to \{⟨1, (X + K) \mod N⟩, ⟨1, (X - K) \mod N⟩\} \notin E$

Metamath Proof Explorer

Theorem gpg5nbgrvtx13starlem2

Proof