gpgedg2iv

Description: The edges of the generalized Petersen graph GPG(N,K) between two inside vertices. (Contributed by AV, 20-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	gpgedg2iv	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \land \{⟨1, X⟩, ⟨1, (Y + K) \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	$⊢ \{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} = \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\}$
6	5	eleq1i	$⊢ \{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \leftrightarrow \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E$
7		uzuzle35	$⊢ N \in ℤ_{\geq 5} \to N \in ℤ_{\geq 3}$
8		simpl	$⊢ (K \in J \land 4 K \mod N \neq 0) \to K \in J$
9	7 8	anim12i	$⊢ (N \in ℤ_{\geq 5} \land (K \in J \land 4 K \mod N \neq 0)) \to (N \in ℤ_{\geq 3} \land K \in J)$
10	9	3adant2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (N \in ℤ_{\geq 3} \land K \in J)$
11	10	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E) \to (N \in ℤ_{\geq 3} \land K \in J)$
12		1ex	$⊢ 1 \in V$
13	12	a1i	$⊢ Y \in I \to 1 \in V$
14	13	anim1i	$⊢ (Y \in I \land X \in I) \to (1 \in V \land X \in I)$
15	14	ancoms	$⊢ (X \in I \land Y \in I) \to (1 \in V \land X \in I)$
16		op1stg	$⊢ (1 \in V \land X \in I) \to 1^{st} (⟨1, X⟩) = 1$
17	15 16	syl	$⊢ (X \in I \land Y \in I) \to 1^{st} (⟨1, X⟩) = 1$
18	17	3ad2ant2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to 1^{st} (⟨1, X⟩) = 1$
19	18	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E) \to 1^{st} (⟨1, X⟩) = 1$
20		simpr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E) \to \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E$
21		eqid	$⊢ Vtx (G) = Vtx (G)$
22	1 3 21 4	gpgvtxedg1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (⟨1, X⟩) = 1 \land \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩)$
23	11 19 20 22	syl3anc	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩)$
24	23	ex	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (\{⟨1, X⟩, ⟨1, (Y - K) \mod N⟩\} \in E \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩))$
25	6 24	biimtrid	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩))$
26	10	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \to (N \in ℤ_{\geq 3} \land K \in J)$
27	18	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \to 1^{st} (⟨1, X⟩) = 1$
28		simpr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \to \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E$
29	1 3 21 4	gpgvtxedg1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (⟨1, X⟩) = 1 \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩)$
30	26 27 28 29	syl3anc	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩)$
31	30	ex	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (\{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩))$
32		ovex	$⊢ (Y + K) \mod N \in V$
33	12 32	opth	$⊢ ⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \leftrightarrow (1 = 1 \land (Y + K) \mod N = (X + K) \mod N)$
34	7	3ad2ant1	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to N \in ℤ_{\geq 3}$
35		simp2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (X \in I \land Y \in I)$
36	35	ancomd	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (Y \in I \land X \in I)$
37		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
38	37 1	eleq2s	$⊢ K \in J \to K \in ℤ$
39	38	adantr	$⊢ (K \in J \land 4 K \mod N \neq 0) \to K \in ℤ$
40	39	3ad2ant3	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to K \in ℤ$
41	2	modaddid	$⊢ (N \in ℤ_{\geq 3} \land (Y \in I \land X \in I) \land K \in ℤ) \to ((Y + K) \mod N = (X + K) \mod N \leftrightarrow Y = X)$
42	34 36 40 41	syl3anc	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((Y + K) \mod N = (X + K) \mod N \leftrightarrow Y = X)$
43	42	biimpa	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land (Y + K) \mod N = (X + K) \mod N) \to Y = X$
44	43	eqcomd	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land (Y + K) \mod N = (X + K) \mod N) \to X = Y$
45	44	ex	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((Y + K) \mod N = (X + K) \mod N \to X = Y)$
46	45	adantld	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((1 = 1 \land (Y + K) \mod N = (X + K) \mod N) \to X = Y)$
47	33 46	biimtrid	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y)$
48	47	a1dd	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y))$
49	12 32	opth	$⊢ ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \leftrightarrow (1 = 0 \land (Y + K) \mod N = X)$
50	49	a1i	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \leftrightarrow (1 = 0 \land (Y + K) \mod N = X))$
51		ax-1ne0	$⊢ 1 \neq 0$
52		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to ((Y + K) \mod N = X \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y)))$
53	51 52	mpi	$⊢ 1 = 0 \to ((Y + K) \mod N = X \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y))$
54	53	imp	$⊢ (1 = 0 \land (Y + K) \mod N = X) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y)$
55	50 54	biimtrdi	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y))$
56	55	imp	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y)$
57		ovex	$⊢ (Y - K) \mod N \in V$
58	12 57	opth	$⊢ ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \leftrightarrow (1 = 0 \land (Y - K) \mod N = X)$
59	58	a1i	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \leftrightarrow (1 = 0 \land (Y - K) \mod N = X))$
60		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to ((Y - K) \mod N = X \to X = Y))$
61	51 60	mpi	$⊢ 1 = 0 \to ((Y - K) \mod N = X \to X = Y)$
62	61	imp	$⊢ (1 = 0 \land (Y - K) \mod N = X) \to X = Y$
63	59 62	biimtrdi	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \to X = Y)$
64	51	orci	$⊢ (1 \neq 0 \lor (Y + K) \mod N \neq X)$
65	12 32	opthne	$⊢ ⟨1, (Y + K) \mod N⟩ \neq ⟨0, X⟩ \leftrightarrow (1 \neq 0 \lor (Y + K) \mod N \neq X)$
66	64 65	mpbir	$⊢ ⟨1, (Y + K) \mod N⟩ \neq ⟨0, X⟩$
67	66	a1i	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ⟨1, (Y + K) \mod N⟩ \neq ⟨0, X⟩$
68		eqneqall	$⊢ ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \to (⟨1, (Y + K) \mod N⟩ \neq ⟨0, X⟩ \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \to X = Y))$
69	67 68	mpan9	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \to X = Y)$
70	56 63 69	3jaod	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y)$
71	70	ex	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y))$
72	12 32	opth	$⊢ ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \leftrightarrow (1 = 1 \land (Y + K) \mod N = (X - K) \mod N)$
73	12 57	opth	$⊢ ⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \leftrightarrow (1 = 1 \land (Y - K) \mod N = (X + K) \mod N)$
74		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
75	7 74	syl	$⊢ N \in ℤ_{\geq 5} \to N \in ℕ$
76	75	adantr	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \to N \in ℕ$
77	76	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \to N \in ℕ$
78		elfzoelz	$⊢ X \in (0 ..^N) \to X \in ℤ$
79	78 2	eleq2s	$⊢ X \in I \to X \in ℤ$
80	79	ad2antrl	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \to X \in ℤ$
81	80	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \to X \in ℤ$
82		elfzoelz	$⊢ Y \in (0 ..^N) \to Y \in ℤ$
83	82 2	eleq2s	$⊢ Y \in I \to Y \in ℤ$
84	83	ad2antll	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \to Y \in ℤ$
85	84	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \to Y \in ℤ$
86	38	adantl	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \to K \in ℤ$
87		modmkpkne	$⊢ (N \in ℕ \land (X \in ℤ \land Y \in ℤ \land K \in ℤ)) \to ((Y - K) \mod N = (X + K) \mod N \to ((Y + K) \mod N = (X - K) \mod N \leftrightarrow 4 K \mod N = 0))$
88	77 81 85 86 87	syl13anc	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \to ((Y - K) \mod N = (X + K) \mod N \to ((Y + K) \mod N = (X - K) \mod N \leftrightarrow 4 K \mod N = 0))$
89	88	imp	$⊢ (((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \land (Y - K) \mod N = (X + K) \mod N) \to ((Y + K) \mod N = (X - K) \mod N \leftrightarrow 4 K \mod N = 0)$
90		eqneqall	$⊢ 4 K \mod N = 0 \to (4 K \mod N \neq 0 \to X = Y)$
91	89 90	biimtrdi	$⊢ (((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \land (Y - K) \mod N = (X + K) \mod N) \to ((Y + K) \mod N = (X - K) \mod N \to (4 K \mod N \neq 0 \to X = Y))$
92	91	expimpd	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \to (((Y - K) \mod N = (X + K) \mod N \land (Y + K) \mod N = (X - K) \mod N) \to (4 K \mod N \neq 0 \to X = Y))$
93	92	com23	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \land K \in J) \to (4 K \mod N \neq 0 \to (((Y - K) \mod N = (X + K) \mod N \land (Y + K) \mod N = (X - K) \mod N) \to X = Y))$
94	93	expimpd	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I)) \to ((K \in J \land 4 K \mod N \neq 0) \to (((Y - K) \mod N = (X + K) \mod N \land (Y + K) \mod N = (X - K) \mod N) \to X = Y))$
95	94	3impia	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (((Y - K) \mod N = (X + K) \mod N \land (Y + K) \mod N = (X - K) \mod N) \to X = Y)$
96	95	expd	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((Y - K) \mod N = (X + K) \mod N \to ((Y + K) \mod N = (X - K) \mod N \to X = Y))$
97	96	adantld	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((1 = 1 \land (Y - K) \mod N = (X + K) \mod N) \to ((Y + K) \mod N = (X - K) \mod N \to X = Y))$
98	73 97	biimtrid	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to ((Y + K) \mod N = (X - K) \mod N \to X = Y))$
99	98	com23	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((Y + K) \mod N = (X - K) \mod N \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y))$
100	99	adantld	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((1 = 1 \land (Y + K) \mod N = (X - K) \mod N) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y))$
101	72 100	biimtrid	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y))$
102	101	imp	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \to X = Y)$
103	51	orci	$⊢ (1 \neq 0 \lor (Y - K) \mod N \neq X)$
104	12 57	opthne	$⊢ ⟨1, (Y - K) \mod N⟩ \neq ⟨0, X⟩ \leftrightarrow (1 \neq 0 \lor (Y - K) \mod N \neq X)$
105	103 104	mpbir	$⊢ ⟨1, (Y - K) \mod N⟩ \neq ⟨0, X⟩$
106		eqneqall	$⊢ ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \to (⟨1, (Y - K) \mod N⟩ \neq ⟨0, X⟩ \to X = Y)$
107	105 106	mpi	$⊢ ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \to X = Y$
108	107	a1i	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \to X = Y)$
109		eqeq2	$⊢ ⟨1, (X - K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩ \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \leftrightarrow ⟨1, (Y - K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩)$
110	109	eqcoms	$⊢ ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \leftrightarrow ⟨1, (Y - K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩)$
111	110	adantl	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \leftrightarrow ⟨1, (Y - K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩)$
112	12 57	opth	$⊢ ⟨1, (Y - K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩ \leftrightarrow (1 = 1 \land (Y - K) \mod N = (Y + K) \mod N)$
113		simpr	$⊢ (X \in I \land Y \in I) \to Y \in I$
114	1 2	modmknepk	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land K \in J) \to (Y - K) \mod N \neq (Y + K) \mod N$
115	7 113 8 114	syl3an	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (Y - K) \mod N \neq (Y + K) \mod N$
116		eqneqall	$⊢ (Y - K) \mod N = (Y + K) \mod N \to ((Y - K) \mod N \neq (Y + K) \mod N \to X = Y)$
117	115 116	syl5com	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((Y - K) \mod N = (Y + K) \mod N \to X = Y)$
118	117	adantld	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((1 = 1 \land (Y - K) \mod N = (Y + K) \mod N) \to X = Y)$
119	112 118	biimtrid	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩ \to X = Y)$
120	119	adantr	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩ \to X = Y)$
121	111 120	sylbid	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \to X = Y)$
122	102 108 121	3jaod	$⊢ ((N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \land ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y)$
123	122	ex	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩ \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y))$
124	48 71 123	3jaod	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y))$
125		op2ndg	$⊢ (1 \in V \land X \in I) \to 2^{nd} (⟨1, X⟩) = X$
126	15 125	syl	$⊢ (X \in I \land Y \in I) \to 2^{nd} (⟨1, X⟩) = X$
127	126	3ad2ant2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to 2^{nd} (⟨1, X⟩) = X$
128		oveq1	$⊢ 2^{nd} (⟨1, X⟩) = X \to 2^{nd} (⟨1, X⟩) + K = X + K$
129	128	oveq1d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (2^{nd} (⟨1, X⟩) + K) \mod N = (X + K) \mod N$
130	129	opeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩$
131	130	eqeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \leftrightarrow ⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩)$
132		opeq2	$⊢ 2^{nd} (⟨1, X⟩) = X \to ⟨0, 2^{nd} (⟨1, X⟩)⟩ = ⟨0, X⟩$
133	132	eqeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \leftrightarrow ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩)$
134		oveq1	$⊢ 2^{nd} (⟨1, X⟩) = X \to 2^{nd} (⟨1, X⟩) - K = X - K$
135	134	oveq1d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (2^{nd} (⟨1, X⟩) - K) \mod N = (X - K) \mod N$
136	135	opeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩$
137	136	eqeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩ \leftrightarrow ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩)$
138	131 133 137	3orbi123d	$⊢ 2^{nd} (⟨1, X⟩) = X \to ((⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \leftrightarrow (⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩))$
139	130	eqeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \leftrightarrow ⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩)$
140	132	eqeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \leftrightarrow ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩)$
141	136	eqeq2d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩ \leftrightarrow ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩)$
142	139 140 141	3orbi123d	$⊢ 2^{nd} (⟨1, X⟩) = X \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \leftrightarrow (⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩))$
143	142	imbi1d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (((⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to X = Y) \leftrightarrow ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y))$
144	138 143	imbi12d	$⊢ 2^{nd} (⟨1, X⟩) = X \to (((⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to X = Y)) \leftrightarrow ((⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y)))$
145	127 144	syl	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (((⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to X = Y)) \leftrightarrow ((⟨1, (Y + K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (X + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, X⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (X - K) \mod N⟩) \to X = Y)))$
146	124 145	mpbird	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y + K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to X = Y))$
147	31 146	syld	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (\{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to X = Y))$
148	147	com23	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) + K) \mod N⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨0, 2^{nd} (⟨1, X⟩)⟩ \lor ⟨1, (Y - K) \mod N⟩ = ⟨1, (2^{nd} (⟨1, X⟩) - K) \mod N⟩) \to (\{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E \to X = Y))$
149	25 148	syld	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \to (\{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E \to X = Y))$
150	149	impd	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \to X = Y)$
151		eqid	$⊢ 1 = 1$
152	151	olci	$⊢ (1 = 0 \lor 1 = 1)$
153	152	2a1i	$⊢ Y \in I \to (X \in I \to (1 = 0 \lor 1 = 1))$
154	153	imdistanri	$⊢ (X \in I \land Y \in I) \to ((1 = 0 \lor 1 = 1) \land Y \in I)$
155	154	3ad2ant2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((1 = 0 \lor 1 = 1) \land Y \in I)$
156	2 1 3 21	opgpgvtx	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (⟨1, Y⟩ \in Vtx (G) \leftrightarrow ((1 = 0 \lor 1 = 1) \land Y \in I))$
157	9 156	syl	$⊢ (N \in ℤ_{\geq 5} \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, Y⟩ \in Vtx (G) \leftrightarrow ((1 = 0 \lor 1 = 1) \land Y \in I))$
158	157	3adant2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (⟨1, Y⟩ \in Vtx (G) \leftrightarrow ((1 = 0 \lor 1 = 1) \land Y \in I))$
159	155 158	mpbird	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ⟨1, Y⟩ \in Vtx (G)$
160	12	a1i	$⊢ X \in I \to 1 \in V$
161		op1stg	$⊢ (1 \in V \land Y \in I) \to 1^{st} (⟨1, Y⟩) = 1$
162	160 161	sylan	$⊢ (X \in I \land Y \in I) \to 1^{st} (⟨1, Y⟩) = 1$
163	162	3ad2ant2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to 1^{st} (⟨1, Y⟩) = 1$
164	1 3 21 4	gpgedgvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (⟨1, Y⟩ \in Vtx (G) \land 1^{st} (⟨1, Y⟩) = 1)) \to (\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨0, 2^{nd} (⟨1, Y⟩)⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E)$
165	10 159 163 164	syl12anc	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨0, 2^{nd} (⟨1, Y⟩)⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E)$
166		op2ndg	$⊢ (1 \in V \land Y \in I) \to 2^{nd} (⟨1, Y⟩) = Y$
167	12 166	mpan	$⊢ Y \in I \to 2^{nd} (⟨1, Y⟩) = Y$
168		oveq1	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to 2^{nd} (⟨1, Y⟩) - K = Y - K$
169	168	oveq1d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to (2^{nd} (⟨1, Y⟩) - K) \mod N = (Y - K) \mod N$
170	169	opeq2d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩ = ⟨1, (Y - K) \mod N⟩$
171	170	preq2d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} = \{⟨1, Y⟩, ⟨1, (Y - K) \mod N⟩\}$
172		prcom	$⊢ \{⟨1, Y⟩, ⟨1, (Y - K) \mod N⟩\} = \{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\}$
173	171 172	eqtrdi	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} = \{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\}$
174	173	eleq1d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to (\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E \leftrightarrow \{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E)$
175		oveq1	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to 2^{nd} (⟨1, Y⟩) + K = Y + K$
176	175	oveq1d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to (2^{nd} (⟨1, Y⟩) + K) \mod N = (Y + K) \mod N$
177	176	opeq2d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩$
178	177	preq2d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} = \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\}$
179	178	eleq1d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to (\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \leftrightarrow \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E)$
180	174 179	anbi12d	$⊢ 2^{nd} (⟨1, Y⟩) = Y \to ((\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E) \leftrightarrow (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
181	167 180	syl	$⊢ Y \in I \to ((\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E) \leftrightarrow (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
182	181	biimpcd	$⊢ (\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E) \to (Y \in I \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
183	182	ancoms	$⊢ (\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E) \to (Y \in I \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
184	183	3adant2	$⊢ (\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨0, 2^{nd} (⟨1, Y⟩)⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E) \to (Y \in I \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
185	184	com12	$⊢ Y \in I \to ((\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨0, 2^{nd} (⟨1, Y⟩)⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E) \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
186	185	adantl	$⊢ (X \in I \land Y \in I) \to ((\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨0, 2^{nd} (⟨1, Y⟩)⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E) \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
187	186	3ad2ant2	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((\{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) + K) \mod N⟩\} \in E \land \{⟨1, Y⟩, ⟨0, 2^{nd} (⟨1, Y⟩)⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (2^{nd} (⟨1, Y⟩) - K) \mod N⟩\} \in E) \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
188	165 187	mpd	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E)$
189		opeq2	$⊢ X = Y \to ⟨1, X⟩ = ⟨1, Y⟩$
190	189	preq2d	$⊢ X = Y \to \{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} = \{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\}$
191	190	eleq1d	$⊢ X = Y \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \leftrightarrow \{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E)$
192	189	preq1d	$⊢ X = Y \to \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} = \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\}$
193	192	eleq1d	$⊢ X = Y \to (\{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E \leftrightarrow \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E)$
194	191 193	anbi12d	$⊢ X = Y \to ((\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \leftrightarrow (\{⟨1, (Y - K) \mod N⟩, ⟨1, Y⟩\} \in E \land \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
195	188 194	syl5ibrcom	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to (X = Y \to (\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E))$
196	150 195	impbid	$⊢ (N \in ℤ_{\geq 5} \land (X \in I \land Y \in I) \land (K \in J \land 4 K \mod N \neq 0)) \to ((\{⟨1, (Y - K) \mod N⟩, ⟨1, X⟩\} \in E \land \{⟨1, X⟩, ⟨1, (Y + K) \mod N⟩\} \in E) \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem gpgedg2iv

Proof