gpgedg2ov

Description: The edges of the generalized Petersen graph GPG(N,K) between two outside vertices. (Contributed by AV, 15-Nov-2025)

	Ref	Expression
Hypotheses	gpgedgiov.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgedgiov.i	$⊢ I = (0 ..^N)$
	gpgedgiov.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpgedgiov.e	$⊢ E = Edg (G)$
Assertion	gpgedg2ov	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		gpgedgiov.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgedgiov.i	$⊢ I = (0 ..^N)$
3		gpgedgiov.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
4		gpgedgiov.e	$⊢ E = Edg (G)$
5		prcom	$⊢ \{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} = \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\}$
6	5	eleq1i	$⊢ \{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \leftrightarrow \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E$
7		uzuzle35	$⊢ N \in ℤ_{\geq 5} \to N \in ℤ_{\geq 3}$
8	7	anim1i	$⊢ (N \in ℤ_{\geq 5} \land K \in J) \to (N \in ℤ_{\geq 3} \land K \in J)$
9	8	adantr	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (N \in ℤ_{\geq 3} \land K \in J)$
10	9	adantr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E) \to (N \in ℤ_{\geq 3} \land K \in J)$
11		c0ex	$⊢ 0 \in V$
12	11	a1i	$⊢ Y \in I \to 0 \in V$
13	12	anim1i	$⊢ (Y \in I \land X \in I) \to (0 \in V \land X \in I)$
14	13	ancoms	$⊢ (X \in I \land Y \in I) \to (0 \in V \land X \in I)$
15		op1stg	$⊢ (0 \in V \land X \in I) \to 1^{st} (⟨0, X⟩) = 0$
16	14 15	syl	$⊢ (X \in I \land Y \in I) \to 1^{st} (⟨0, X⟩) = 0$
17	16	adantl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to 1^{st} (⟨0, X⟩) = 0$
18	17	adantr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E) \to 1^{st} (⟨0, X⟩) = 0$
19		simpr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E) \to \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E$
20		eqid	$⊢ Vtx (G) = Vtx (G)$
21	1 3 20 4	gpgvtxedg0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (⟨0, X⟩) = 0 \land \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩)$
22	10 18 19 21	syl3anc	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩)$
23	22	ex	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, X⟩, ⟨0, (Y - 1) \mod N⟩\} \in E \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩))$
24	6 23	biimtrid	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩))$
25	9	adantr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \to (N \in ℤ_{\geq 3} \land K \in J)$
26	17	adantr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \to 1^{st} (⟨0, X⟩) = 0$
27		simpr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \to \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E$
28	1 3 20 4	gpgvtxedg0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (⟨0, X⟩) = 0 \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩)$
29	25 26 27 28	syl3anc	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩)$
30	29	ex	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩))$
31		ovex	$⊢ (Y + 1) \mod N \in V$
32	11 31	opth	$⊢ ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \leftrightarrow (0 = 0 \land (Y + 1) \mod N = (X + 1) \mod N)$
33	7	adantr	$⊢ (N \in ℤ_{\geq 5} \land K \in J) \to N \in ℤ_{\geq 3}$
34	33	adantr	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to N \in ℤ_{\geq 3}$
35		simpr	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (X \in I \land Y \in I)$
36	35	ancomd	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (Y \in I \land X \in I)$
37		1zzd	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to 1 \in ℤ$
38	2	modaddid	$⊢ (N \in ℤ_{\geq 3} \land (Y \in I \land X \in I) \land 1 \in ℤ) \to ((Y + 1) \mod N = (X + 1) \mod N \leftrightarrow Y = X)$
39	34 36 37 38	syl3anc	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((Y + 1) \mod N = (X + 1) \mod N \leftrightarrow Y = X)$
40	39	biimpa	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land (Y + 1) \mod N = (X + 1) \mod N) \to Y = X$
41	40	eqcomd	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land (Y + 1) \mod N = (X + 1) \mod N) \to X = Y$
42	41	ex	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((Y + 1) \mod N = (X + 1) \mod N \to X = Y)$
43	42	adantld	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((0 = 0 \land (Y + 1) \mod N = (X + 1) \mod N) \to X = Y)$
44	32 43	biimtrid	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y)$
45	44	imp	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩) \to X = Y$
46	45	a1d	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y)$
47	46	ex	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y))$
48	11 31	opth	$⊢ ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \leftrightarrow (0 = 1 \land (Y + 1) \mod N = X)$
49		0ne1	$⊢ 0 \neq 1$
50		eqneqall	$⊢ 0 = 1 \to (0 \neq 1 \to ((Y + 1) \mod N = X \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y)))$
51	49 50	mpi	$⊢ 0 = 1 \to ((Y + 1) \mod N = X \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y))$
52	51	imp	$⊢ (0 = 1 \land (Y + 1) \mod N = X) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y)$
53	52	a1i	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((0 = 1 \land (Y + 1) \mod N = X) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y))$
54	48 53	biimtrid	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y))$
55	54	imp	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y)$
56		eqeq2	$⊢ ⟨1, X⟩ = ⟨0, (Y + 1) \mod N⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩)$
57	56	eqcoms	$⊢ ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩)$
58	57	adantl	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩)$
59		ovex	$⊢ (Y - 1) \mod N \in V$
60	11 59	opth	$⊢ ⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩ \leftrightarrow (0 = 0 \land (Y - 1) \mod N = (Y + 1) \mod N)$
61		simpr	$⊢ (X \in I \land Y \in I) \to Y \in I$
62	2	modm1nep1	$⊢ (N \in ℤ_{\geq 3} \land Y \in I) \to (Y - 1) \mod N \neq (Y + 1) \mod N$
63	33 61 62	syl2an	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (Y - 1) \mod N \neq (Y + 1) \mod N$
64		eqneqall	$⊢ (Y - 1) \mod N = (Y + 1) \mod N \to ((Y - 1) \mod N \neq (Y + 1) \mod N \to X = Y)$
65	64	com12	$⊢ (Y - 1) \mod N \neq (Y + 1) \mod N \to ((Y - 1) \mod N = (Y + 1) \mod N \to X = Y)$
66	63 65	syl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((Y - 1) \mod N = (Y + 1) \mod N \to X = Y)$
67	66	adantld	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((0 = 0 \land (Y - 1) \mod N = (Y + 1) \mod N) \to X = Y)$
68	60 67	biimtrid	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩ \to X = Y)$
69	68	adantr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩ \to X = Y)$
70	58 69	sylbid	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \to X = Y)$
71	49	orci	$⊢ (0 \neq 1 \lor (Y + 1) \mod N \neq X)$
72	11 31	opthne	$⊢ ⟨0, (Y + 1) \mod N⟩ \neq ⟨1, X⟩ \leftrightarrow (0 \neq 1 \lor (Y + 1) \mod N \neq X)$
73	71 72	mpbir	$⊢ ⟨0, (Y + 1) \mod N⟩ \neq ⟨1, X⟩$
74	73	a1i	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ⟨0, (Y + 1) \mod N⟩ \neq ⟨1, X⟩$
75		eqneqall	$⊢ ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \to (⟨0, (Y + 1) \mod N⟩ \neq ⟨1, X⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to X = Y))$
76	75	com12	$⊢ ⟨0, (Y + 1) \mod N⟩ \neq ⟨1, X⟩ \to (⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to X = Y))$
77	74 76	syl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to X = Y))$
78	77	imp	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to X = Y)$
79	55 70 78	3jaod	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y)$
80	79	ex	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y))$
81	11 31	opth	$⊢ ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \leftrightarrow (0 = 0 \land (Y + 1) \mod N = (X - 1) \mod N)$
82	11 59	opth	$⊢ ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \leftrightarrow (0 = 0 \land (Y - 1) \mod N = (X + 1) \mod N)$
83		simpll	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to N \in ℤ_{\geq 5}$
84		simprl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to X \in I$
85		simprr	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to Y \in I$
86	2	modm1p1ne	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to ((Y - 1) \mod N = (X + 1) \mod N \to (Y + 1) \mod N \neq (X - 1) \mod N)$
87	83 84 85 86	syl3anc	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((Y - 1) \mod N = (X + 1) \mod N \to (Y + 1) \mod N \neq (X - 1) \mod N)$
88		eqneqall	$⊢ (Y + 1) \mod N = (X - 1) \mod N \to ((Y + 1) \mod N \neq (X - 1) \mod N \to X = Y)$
89	88	com12	$⊢ (Y + 1) \mod N \neq (X - 1) \mod N \to ((Y + 1) \mod N = (X - 1) \mod N \to X = Y)$
90	89	a1i	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((Y + 1) \mod N \neq (X - 1) \mod N \to ((Y + 1) \mod N = (X - 1) \mod N \to X = Y))$
91	87 90	syld	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((Y - 1) \mod N = (X + 1) \mod N \to ((Y + 1) \mod N = (X - 1) \mod N \to X = Y))$
92	91	adantld	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((0 = 0 \land (Y - 1) \mod N = (X + 1) \mod N) \to ((Y + 1) \mod N = (X - 1) \mod N \to X = Y))$
93	82 92	biimtrid	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to ((Y + 1) \mod N = (X - 1) \mod N \to X = Y))$
94	93	com23	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((Y + 1) \mod N = (X - 1) \mod N \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y))$
95	94	adantld	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((0 = 0 \land (Y + 1) \mod N = (X - 1) \mod N) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y))$
96	81 95	biimtrid	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y))$
97	96	imp	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y)$
98	49	orci	$⊢ (0 \neq 1 \lor (Y - 1) \mod N \neq X)$
99	11 59	opthne	$⊢ ⟨0, (Y - 1) \mod N⟩ \neq ⟨1, X⟩ \leftrightarrow (0 \neq 1 \lor (Y - 1) \mod N \neq X)$
100	98 99	mpbir	$⊢ ⟨0, (Y - 1) \mod N⟩ \neq ⟨1, X⟩$
101		eqneqall	$⊢ ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \to (⟨0, (Y - 1) \mod N⟩ \neq ⟨1, X⟩ \to X = Y)$
102	100 101	mpi	$⊢ ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \to X = Y$
103	102	a1i	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \to X = Y)$
104		eqeq2	$⊢ ⟨0, (X - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩)$
105	104	eqcoms	$⊢ ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩)$
106	105	adantl	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩)$
107	68	adantr	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩ \to X = Y)$
108	106 107	sylbid	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to X = Y)$
109	97 103 108	3jaod	$⊢ (((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \land ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y)$
110	109	ex	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩ \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y))$
111	47 80 110	3jaod	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y))$
112		op2ndg	$⊢ (0 \in V \land X \in I) \to 2^{nd} (⟨0, X⟩) = X$
113	11 112	mpan	$⊢ X \in I \to 2^{nd} (⟨0, X⟩) = X$
114	113	adantr	$⊢ (X \in I \land Y \in I) \to 2^{nd} (⟨0, X⟩) = X$
115	114	adantl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to 2^{nd} (⟨0, X⟩) = X$
116		oveq1	$⊢ 2^{nd} (⟨0, X⟩) = X \to 2^{nd} (⟨0, X⟩) + 1 = X + 1$
117	116	oveq1d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (2^{nd} (⟨0, X⟩) + 1) \mod N = (X + 1) \mod N$
118	117	opeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩$
119	118	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \leftrightarrow ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩)$
120		opeq2	$⊢ 2^{nd} (⟨0, X⟩) = X \to ⟨1, 2^{nd} (⟨0, X⟩)⟩ = ⟨1, X⟩$
121	120	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \leftrightarrow ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩)$
122		oveq1	$⊢ 2^{nd} (⟨0, X⟩) = X \to 2^{nd} (⟨0, X⟩) - 1 = X - 1$
123	122	oveq1d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (2^{nd} (⟨0, X⟩) - 1) \mod N = (X - 1) \mod N$
124	123	opeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩$
125	124	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩ \leftrightarrow ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩)$
126	119 121 125	3orbi123d	$⊢ 2^{nd} (⟨0, X⟩) = X \to ((⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \leftrightarrow (⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩))$
127	118	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩)$
128	120	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩)$
129	124	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩ \leftrightarrow ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩)$
130	127 128 129	3orbi123d	$⊢ 2^{nd} (⟨0, X⟩) = X \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \leftrightarrow (⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩))$
131	130	imbi1d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (((⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y) \leftrightarrow ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y))$
132	126 131	imbi12d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (((⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y)) \leftrightarrow ((⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y)))$
133	115 132	syl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (((⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y)) \leftrightarrow ((⟨0, (Y + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, X⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y)))$
134	111 133	mpbird	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y + 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y))$
135	30 134	syld	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y))$
136	135	com23	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨0, (Y - 1) \mod N⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to (\{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E \to X = Y))$
137	24 136	syld	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \to (\{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E \to X = Y))$
138	137	impd	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \to X = Y)$
139		eqid	$⊢ 0 = 0$
140	139	orci	$⊢ (0 = 0 \lor 0 = 1)$
141	61 140	jctil	$⊢ (X \in I \land Y \in I) \to ((0 = 0 \lor 0 = 1) \land Y \in I)$
142	141	adantl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((0 = 0 \lor 0 = 1) \land Y \in I)$
143	2 1 3 20	opgpgvtx	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (⟨0, Y⟩ \in Vtx (G) \leftrightarrow ((0 = 0 \lor 0 = 1) \land Y \in I))$
144	8 143	syl	$⊢ (N \in ℤ_{\geq 5} \land K \in J) \to (⟨0, Y⟩ \in Vtx (G) \leftrightarrow ((0 = 0 \lor 0 = 1) \land Y \in I))$
145	144	adantr	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (⟨0, Y⟩ \in Vtx (G) \leftrightarrow ((0 = 0 \lor 0 = 1) \land Y \in I))$
146	142 145	mpbird	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ⟨0, Y⟩ \in Vtx (G)$
147	11	a1i	$⊢ X \in I \to 0 \in V$
148		op1stg	$⊢ (0 \in V \land Y \in I) \to 1^{st} (⟨0, Y⟩) = 0$
149	147 148	sylan	$⊢ (X \in I \land Y \in I) \to 1^{st} (⟨0, Y⟩) = 0$
150	149	adantl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to 1^{st} (⟨0, Y⟩) = 0$
151	1 3 20 4	gpgedgvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (⟨0, Y⟩ \in Vtx (G) \land 1^{st} (⟨0, Y⟩) = 0)) \to (\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨1, 2^{nd} (⟨0, Y⟩)⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E)$
152	9 146 150 151	syl12anc	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨1, 2^{nd} (⟨0, Y⟩)⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E)$
153		op2ndg	$⊢ (0 \in V \land Y \in I) \to 2^{nd} (⟨0, Y⟩) = Y$
154	11 153	mpan	$⊢ Y \in I \to 2^{nd} (⟨0, Y⟩) = Y$
155		oveq1	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to 2^{nd} (⟨0, Y⟩) - 1 = Y - 1$
156	155	oveq1d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to (2^{nd} (⟨0, Y⟩) - 1) \mod N = (Y - 1) \mod N$
157	156	opeq2d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩ = ⟨0, (Y - 1) \mod N⟩$
158	157	preq2d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} = \{⟨0, Y⟩, ⟨0, (Y - 1) \mod N⟩\}$
159		prcom	$⊢ \{⟨0, Y⟩, ⟨0, (Y - 1) \mod N⟩\} = \{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\}$
160	158 159	eqtrdi	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} = \{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\}$
161	160	eleq1d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to (\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E \leftrightarrow \{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E)$
162		oveq1	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to 2^{nd} (⟨0, Y⟩) + 1 = Y + 1$
163	162	oveq1d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to (2^{nd} (⟨0, Y⟩) + 1) \mod N = (Y + 1) \mod N$
164	163	opeq2d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩$
165	164	preq2d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} = \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\}$
166	165	eleq1d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to (\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \leftrightarrow \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E)$
167	161 166	anbi12d	$⊢ 2^{nd} (⟨0, Y⟩) = Y \to ((\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E) \leftrightarrow (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
168	154 167	syl	$⊢ Y \in I \to ((\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E) \leftrightarrow (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
169	168	biimpcd	$⊢ (\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E) \to (Y \in I \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
170	169	ancoms	$⊢ (\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E) \to (Y \in I \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
171	170	3adant2	$⊢ (\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨1, 2^{nd} (⟨0, Y⟩)⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E) \to (Y \in I \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
172	171	com12	$⊢ Y \in I \to ((\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨1, 2^{nd} (⟨0, Y⟩)⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E) \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
173	172	adantl	$⊢ (X \in I \land Y \in I) \to ((\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨1, 2^{nd} (⟨0, Y⟩)⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E) \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
174	173	adantl	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((\{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) + 1) \mod N⟩\} \in E \land \{⟨0, Y⟩, ⟨1, 2^{nd} (⟨0, Y⟩)⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (2^{nd} (⟨0, Y⟩) - 1) \mod N⟩\} \in E) \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
175	152 174	mpd	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E)$
176		opeq2	$⊢ X = Y \to ⟨0, X⟩ = ⟨0, Y⟩$
177	176	preq2d	$⊢ X = Y \to \{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} = \{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\}$
178	177	eleq1d	$⊢ X = Y \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \leftrightarrow \{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E)$
179	176	preq1d	$⊢ X = Y \to \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} = \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\}$
180	179	eleq1d	$⊢ X = Y \to (\{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E \leftrightarrow \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E)$
181	178 180	anbi12d	$⊢ X = Y \to ((\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \leftrightarrow (\{⟨0, (Y - 1) \mod N⟩, ⟨0, Y⟩\} \in E \land \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
182	175 181	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to (X = Y \to (\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E))$
183	138 182	impbid	$⊢ ((N \in ℤ_{\geq 5} \land K \in J) \land (X \in I \land Y \in I)) \to ((\{⟨0, (Y - 1) \mod N⟩, ⟨0, X⟩\} \in E \land \{⟨0, X⟩, ⟨0, (Y + 1) \mod N⟩\} \in E) \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem gpgedg2ov

Proof