gpgedgvtx0

Description: The edges starting at an outside vertex in a generalized Petersen graph G . (Contributed by AV, 29-Aug-2025)

	Ref	Expression
Hypotheses	gpgedgvtx0.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgedgvtx0.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpgedgvtx0.v	$⊢ V = Vtx (G)$
	gpgedgvtx0.e	$⊢ E = Edg (G)$
Assertion	gpgedgvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E)$

Proof

Step	Hyp	Ref	Expression
1		gpgedgvtx0.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgedgvtx0.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
3		gpgedgvtx0.v	$⊢ V = Vtx (G)$
4		gpgedgvtx0.e	$⊢ E = Edg (G)$
5		eqid	$⊢ (0 ..^N) = (0 ..^N)$
6	5 1 2 3	gpgvtxel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \leftrightarrow \exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩)$
7		fveq2	$⊢ X = ⟨x, y⟩ \to 1^{st} (X) = 1^{st} (⟨x, y⟩)$
8	7	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land X = ⟨x, y⟩) \to 1^{st} (X) = 1^{st} (⟨x, y⟩)$
9		vex	$⊢ x \in V$
10		vex	$⊢ y \in V$
11	9 10	op1st	$⊢ 1^{st} (⟨x, y⟩) = x$
12	8 11	eqtrdi	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land X = ⟨x, y⟩) \to 1^{st} (X) = x$
13	12	eqeq1d	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land X = ⟨x, y⟩) \to (1^{st} (X) = 0 \leftrightarrow x = 0)$
14		opeq1	$⊢ x = 0 \to ⟨x, y⟩ = ⟨0, y⟩$
15	14	eqeq2d	$⊢ x = 0 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨0, y⟩)$
16	15	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land x = 0) \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨0, y⟩)$
17		simpr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to y \in (0 ..^N)$
18		opeq2	$⊢ z = y \to ⟨0, z⟩ = ⟨0, y⟩$
19		oveq1	$⊢ z = y \to z + 1 = y + 1$
20	19	oveq1d	$⊢ z = y \to (z + 1) \mod N = (y + 1) \mod N$
21	20	opeq2d	$⊢ z = y \to ⟨0, (z + 1) \mod N⟩ = ⟨0, (y + 1) \mod N⟩$
22	18 21	preq12d	$⊢ z = y \to \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\}$
23	22	eqeq2d	$⊢ z = y \to (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\})$
24		opeq2	$⊢ z = y \to ⟨1, z⟩ = ⟨1, y⟩$
25	18 24	preq12d	$⊢ z = y \to \{⟨0, z⟩, ⟨1, z⟩\} = \{⟨0, y⟩, ⟨1, y⟩\}$
26	25	eqeq2d	$⊢ z = y \to (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\})$
27		oveq1	$⊢ z = y \to z + K = y + K$
28	27	oveq1d	$⊢ z = y \to (z + K) \mod N = (y + K) \mod N$
29	28	opeq2d	$⊢ z = y \to ⟨1, (z + K) \mod N⟩ = ⟨1, (y + K) \mod N⟩$
30	24 29	preq12d	$⊢ z = y \to \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}$
31	30	eqeq2d	$⊢ z = y \to (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
32	23 26 31	3orbi123d	$⊢ z = y \to ((\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
33	32	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \land z = y) \to ((\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
34		eqid	$⊢ \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\}$
35	34	3mix1i	$⊢ (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
36	35	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
37	17 33 36	rspcedvd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
38	22	eqeq2d	$⊢ z = y \to (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\})$
39	25	eqeq2d	$⊢ z = y \to (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\})$
40	30	eqeq2d	$⊢ z = y \to (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
41	38 39 40	3orbi123d	$⊢ z = y \to ((\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
42	41	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \land z = y) \to ((\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
43		eqid	$⊢ \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\}$
44	43	3mix2i	$⊢ (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
45	44	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
46	17 42 45	rspcedvd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
47		elfzo0l	$⊢ y \in (0 ..^N) \to (y = 0 \lor y \in (1 ..^N))$
48		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
49	48	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y = 0) \to N \in ℕ$
50		fzo0end	$⊢ N \in ℕ \to N - 1 \in (0 ..^N)$
51	49 50	syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y = 0) \to N - 1 \in (0 ..^N)$
52		opeq2	$⊢ y = 0 \to ⟨0, y⟩ = ⟨0, 0⟩$
53		oveq1	$⊢ y = 0 \to y - 1 = 0 - 1$
54	53	oveq1d	$⊢ y = 0 \to (y - 1) \mod N = (0 - 1) \mod N$
55	54	opeq2d	$⊢ y = 0 \to ⟨0, (y - 1) \mod N⟩ = ⟨0, (0 - 1) \mod N⟩$
56	52 55	preq12d	$⊢ y = 0 \to \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\}$
57		opeq2	$⊢ z = N - 1 \to ⟨0, z⟩ = ⟨0, N - 1⟩$
58		oveq1	$⊢ z = N - 1 \to z + 1 = N - 1 + 1$
59	58	oveq1d	$⊢ z = N - 1 \to (z + 1) \mod N = (N - 1 + 1) \mod N$
60	59	opeq2d	$⊢ z = N - 1 \to ⟨0, (z + 1) \mod N⟩ = ⟨0, (N - 1 + 1) \mod N⟩$
61	57 60	preq12d	$⊢ z = N - 1 \to \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨0, (N - 1 + 1) \mod N⟩\}$
62	56 61	eqeqan12d	$⊢ (y = 0 \land z = N - 1) \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨0, (N - 1 + 1) \mod N⟩\})$
63		opeq2	$⊢ z = N - 1 \to ⟨1, z⟩ = ⟨1, N - 1⟩$
64	57 63	preq12d	$⊢ z = N - 1 \to \{⟨0, z⟩, ⟨1, z⟩\} = \{⟨0, N - 1⟩, ⟨1, N - 1⟩\}$
65	56 64	eqeqan12d	$⊢ (y = 0 \land z = N - 1) \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨1, N - 1⟩\})$
66		oveq1	$⊢ z = N - 1 \to z + K = N - 1 + K$
67	66	oveq1d	$⊢ z = N - 1 \to (z + K) \mod N = (N - 1 + K) \mod N$
68	67	opeq2d	$⊢ z = N - 1 \to ⟨1, (z + K) \mod N⟩ = ⟨1, (N - 1 + K) \mod N⟩$
69	63 68	preq12d	$⊢ z = N - 1 \to \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} = \{⟨1, N - 1⟩, ⟨1, (N - 1 + K) \mod N⟩\}$
70	56 69	eqeqan12d	$⊢ (y = 0 \land z = N - 1) \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨1, N - 1⟩, ⟨1, (N - 1 + K) \mod N⟩\})$
71	62 65 70	3orbi123d	$⊢ (y = 0 \land z = N - 1) \to ((\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨0, (N - 1 + 1) \mod N⟩\} \lor \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨1, N - 1⟩\} \lor \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨1, N - 1⟩, ⟨1, (N - 1 + K) \mod N⟩\}))$
72	71	adantll	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y = 0) \land z = N - 1) \to ((\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨0, (N - 1 + 1) \mod N⟩\} \lor \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨1, N - 1⟩\} \lor \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨1, N - 1⟩, ⟨1, (N - 1 + K) \mod N⟩\}))$
73		nncn	$⊢ N \in ℕ \to N \in ℂ$
74		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
75	48 73 74	3syl	$⊢ N \in ℤ_{\geq 3} \to N - 1 + 1 = N$
76	75	oveq1d	$⊢ N \in ℤ_{\geq 3} \to (N - 1 + 1) \mod N = N \mod N$
77		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
78		modid0	$⊢ N \in ℝ^{+} \to N \mod N = 0$
79	48 77 78	3syl	$⊢ N \in ℤ_{\geq 3} \to N \mod N = 0$
80	76 79	eqtr2d	$⊢ N \in ℤ_{\geq 3} \to 0 = (N - 1 + 1) \mod N$
81	80	opeq2d	$⊢ N \in ℤ_{\geq 3} \to ⟨0, 0⟩ = ⟨0, (N - 1 + 1) \mod N⟩$
82		df-neg	$⊢ - 1 = 0 - 1$
83	82	eqcomi	$⊢ 0 - 1 = - 1$
84	83	a1i	$⊢ N \in ℤ_{\geq 3} \to 0 - 1 = - 1$
85	84	oveq1d	$⊢ N \in ℤ_{\geq 3} \to (0 - 1) \mod N = -1 \mod N$
86		m1modnnsub1	$⊢ N \in ℕ \to -1 \mod N = N - 1$
87	48 86	syl	$⊢ N \in ℤ_{\geq 3} \to -1 \mod N = N - 1$
88	85 87	eqtrd	$⊢ N \in ℤ_{\geq 3} \to (0 - 1) \mod N = N - 1$
89	88	opeq2d	$⊢ N \in ℤ_{\geq 3} \to ⟨0, (0 - 1) \mod N⟩ = ⟨0, N - 1⟩$
90	81 89	preq12d	$⊢ N \in ℤ_{\geq 3} \to \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, (N - 1 + 1) \mod N⟩, ⟨0, N - 1⟩\}$
91	90	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y = 0) \to \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, (N - 1 + 1) \mod N⟩, ⟨0, N - 1⟩\}$
92		prcom	$⊢ \{⟨0, (N - 1 + 1) \mod N⟩, ⟨0, N - 1⟩\} = \{⟨0, N - 1⟩, ⟨0, (N - 1 + 1) \mod N⟩\}$
93	91 92	eqtrdi	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y = 0) \to \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨0, (N - 1 + 1) \mod N⟩\}$
94	93	3mix1d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y = 0) \to (\{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨0, (N - 1 + 1) \mod N⟩\} \lor \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨0, N - 1⟩, ⟨1, N - 1⟩\} \lor \{⟨0, 0⟩, ⟨0, (0 - 1) \mod N⟩\} = \{⟨1, N - 1⟩, ⟨1, (N - 1 + K) \mod N⟩\})$
95	51 72 94	rspcedvd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y = 0) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
96	95	expcom	$⊢ y = 0 \to ((N \in ℤ_{\geq 3} \land K \in J) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
97		elfzofz	$⊢ y \in (1 ..^N) \to y \in (1 \dots N)$
98		fz1fzo0m1	$⊢ y \in (1 \dots N) \to y - 1 \in (0 ..^N)$
99	97 98	syl	$⊢ y \in (1 ..^N) \to y - 1 \in (0 ..^N)$
100	99	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to y - 1 \in (0 ..^N)$
101		opeq2	$⊢ z = y - 1 \to ⟨0, z⟩ = ⟨0, y - 1⟩$
102		oveq1	$⊢ z = y - 1 \to z + 1 = y - 1 + 1$
103	102	oveq1d	$⊢ z = y - 1 \to (z + 1) \mod N = (y - 1 + 1) \mod N$
104	103	opeq2d	$⊢ z = y - 1 \to ⟨0, (z + 1) \mod N⟩ = ⟨0, (y - 1 + 1) \mod N⟩$
105	101 104	preq12d	$⊢ z = y - 1 \to \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨0, (y - 1 + 1) \mod N⟩\}$
106	105	eqeq2d	$⊢ z = y - 1 \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨0, (y - 1 + 1) \mod N⟩\})$
107		opeq2	$⊢ z = y - 1 \to ⟨1, z⟩ = ⟨1, y - 1⟩$
108	101 107	preq12d	$⊢ z = y - 1 \to \{⟨0, z⟩, ⟨1, z⟩\} = \{⟨0, y - 1⟩, ⟨1, y - 1⟩\}$
109	108	eqeq2d	$⊢ z = y - 1 \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨1, y - 1⟩\})$
110		oveq1	$⊢ z = y - 1 \to z + K = y - 1 + K$
111	110	oveq1d	$⊢ z = y - 1 \to (z + K) \mod N = (y - 1 + K) \mod N$
112	111	opeq2d	$⊢ z = y - 1 \to ⟨1, (z + K) \mod N⟩ = ⟨1, (y - 1 + K) \mod N⟩$
113	107 112	preq12d	$⊢ z = y - 1 \to \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} = \{⟨1, y - 1⟩, ⟨1, (y - 1 + K) \mod N⟩\}$
114	113	eqeq2d	$⊢ z = y - 1 \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, y - 1⟩, ⟨1, (y - 1 + K) \mod N⟩\})$
115	106 109 114	3orbi123d	$⊢ z = y - 1 \to ((\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨0, (y - 1 + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨1, y - 1⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, y - 1⟩, ⟨1, (y - 1 + K) \mod N⟩\}))$
116	115	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \land z = y - 1) \to ((\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨0, (y - 1 + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨1, y - 1⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, y - 1⟩, ⟨1, (y - 1 + K) \mod N⟩\}))$
117		elfzoelz	$⊢ y \in (1 ..^N) \to y \in ℤ$
118		zcn	$⊢ y \in ℤ \to y \in ℂ$
119		npcan1	$⊢ y \in ℂ \to y - 1 + 1 = y$
120	117 118 119	3syl	$⊢ y \in (1 ..^N) \to y - 1 + 1 = y$
121	120	oveq1d	$⊢ y \in (1 ..^N) \to (y - 1 + 1) \mod N = y \mod N$
122		elfzo1	$⊢ y \in (1 ..^N) \leftrightarrow (y \in ℕ \land N \in ℕ \land y < N)$
123		nnre	$⊢ y \in ℕ \to y \in ℝ$
124	123 77	anim12i	$⊢ (y \in ℕ \land N \in ℕ) \to (y \in ℝ \land N \in ℝ^{+})$
125	124	3adant3	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to (y \in ℝ \land N \in ℝ^{+})$
126		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
127	126	nn0ge0d	$⊢ y \in ℕ \to 0 \leq y$
128	127	anim1i	$⊢ (y \in ℕ \land y < N) \to (0 \leq y \land y < N)$
129	128	3adant2	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to (0 \leq y \land y < N)$
130	125 129	jca	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to ((y \in ℝ \land N \in ℝ^{+}) \land (0 \leq y \land y < N))$
131	122 130	sylbi	$⊢ y \in (1 ..^N) \to ((y \in ℝ \land N \in ℝ^{+}) \land (0 \leq y \land y < N))$
132		modid	$⊢ ((y \in ℝ \land N \in ℝ^{+}) \land (0 \leq y \land y < N)) \to y \mod N = y$
133	131 132	syl	$⊢ y \in (1 ..^N) \to y \mod N = y$
134	121 133	eqtrd	$⊢ y \in (1 ..^N) \to (y - 1 + 1) \mod N = y$
135	134	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to (y - 1 + 1) \mod N = y$
136	135	eqcomd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to y = (y - 1 + 1) \mod N$
137	136	opeq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to ⟨0, y⟩ = ⟨0, (y - 1 + 1) \mod N⟩$
138		1red	$⊢ y \in ℕ \to 1 \in ℝ$
139	123 138	resubcld	$⊢ y \in ℕ \to y - 1 \in ℝ$
140	139 77	anim12i	$⊢ (y \in ℕ \land N \in ℕ) \to (y - 1 \in ℝ \land N \in ℝ^{+})$
141	140	3adant3	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to (y - 1 \in ℝ \land N \in ℝ^{+})$
142		nnm1ge0	$⊢ y \in ℕ \to 0 \leq y - 1$
143	142	3ad2ant1	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to 0 \leq y - 1$
144	139	3ad2ant1	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to y - 1 \in ℝ$
145	123	3ad2ant1	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to y \in ℝ$
146		nnre	$⊢ N \in ℕ \to N \in ℝ$
147	146	3ad2ant2	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to N \in ℝ$
148	123	ltm1d	$⊢ y \in ℕ \to y - 1 < y$
149	148	3ad2ant1	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to y - 1 < y$
150		simp3	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to y < N$
151	144 145 147 149 150	lttrd	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to y - 1 < N$
152	141 143 151	jca32	$⊢ (y \in ℕ \land N \in ℕ \land y < N) \to ((y - 1 \in ℝ \land N \in ℝ^{+}) \land (0 \leq y - 1 \land y - 1 < N))$
153	122 152	sylbi	$⊢ y \in (1 ..^N) \to ((y - 1 \in ℝ \land N \in ℝ^{+}) \land (0 \leq y - 1 \land y - 1 < N))$
154	153	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to ((y - 1 \in ℝ \land N \in ℝ^{+}) \land (0 \leq y - 1 \land y - 1 < N))$
155		modid	$⊢ ((y - 1 \in ℝ \land N \in ℝ^{+}) \land (0 \leq y - 1 \land y - 1 < N)) \to (y - 1) \mod N = y - 1$
156	154 155	syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to (y - 1) \mod N = y - 1$
157	156	opeq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to ⟨0, (y - 1) \mod N⟩ = ⟨0, y - 1⟩$
158	137 157	preq12d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, (y - 1 + 1) \mod N⟩, ⟨0, y - 1⟩\}$
159		prcom	$⊢ \{⟨0, (y - 1 + 1) \mod N⟩, ⟨0, y - 1⟩\} = \{⟨0, y - 1⟩, ⟨0, (y - 1 + 1) \mod N⟩\}$
160	158 159	eqtrdi	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨0, (y - 1 + 1) \mod N⟩\}$
161	160	3mix1d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨0, (y - 1 + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, y - 1⟩, ⟨1, y - 1⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, y - 1⟩, ⟨1, (y - 1 + K) \mod N⟩\})$
162	100 116 161	rspcedvd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (1 ..^N)) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
163	162	expcom	$⊢ y \in (1 ..^N) \to ((N \in ℤ_{\geq 3} \land K \in J) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
164	96 163	jaoi	$⊢ (y = 0 \lor y \in (1 ..^N)) \to ((N \in ℤ_{\geq 3} \land K \in J) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
165	47 164	syl	$⊢ y \in (0 ..^N) \to ((N \in ℤ_{\geq 3} \land K \in J) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
166	165	impcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
167	5 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \in E \leftrightarrow \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
168	5 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨0, y⟩, ⟨1, y⟩\} \in E \leftrightarrow \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
169	5 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} \in E \leftrightarrow \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
170	167 168 169	3anbi123d	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to ((\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \in E \land \{⟨0, y⟩, ⟨1, y⟩\} \in E \land \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} \in E) \leftrightarrow (\exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})))$
171	170	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to ((\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \in E \land \{⟨0, y⟩, ⟨1, y⟩\} \in E \land \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} \in E) \leftrightarrow (\exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨1, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})))$
172	37 46 166 171	mpbir3and	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \in E \land \{⟨0, y⟩, ⟨1, y⟩\} \in E \land \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} \in E)$
173	172	adantrl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \in E \land \{⟨0, y⟩, ⟨1, y⟩\} \in E \land \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} \in E)$
174		id	$⊢ X = ⟨0, y⟩ \to X = ⟨0, y⟩$
175		c0ex	$⊢ 0 \in V$
176	175 10	op2ndd	$⊢ X = ⟨0, y⟩ \to 2^{nd} (X) = y$
177	176	oveq1d	$⊢ X = ⟨0, y⟩ \to 2^{nd} (X) + 1 = y + 1$
178	177	oveq1d	$⊢ X = ⟨0, y⟩ \to (2^{nd} (X) + 1) \mod N = (y + 1) \mod N$
179	178	opeq2d	$⊢ X = ⟨0, y⟩ \to ⟨0, (2^{nd} (X) + 1) \mod N⟩ = ⟨0, (y + 1) \mod N⟩$
180	174 179	preq12d	$⊢ X = ⟨0, y⟩ \to \{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\}$
181	180	eleq1d	$⊢ X = ⟨0, y⟩ \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \in E)$
182	176	opeq2d	$⊢ X = ⟨0, y⟩ \to ⟨1, 2^{nd} (X)⟩ = ⟨1, y⟩$
183	174 182	preq12d	$⊢ X = ⟨0, y⟩ \to \{X, ⟨1, 2^{nd} (X)⟩\} = \{⟨0, y⟩, ⟨1, y⟩\}$
184	183	eleq1d	$⊢ X = ⟨0, y⟩ \to (\{X, ⟨1, 2^{nd} (X)⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨1, y⟩\} \in E)$
185	176	oveq1d	$⊢ X = ⟨0, y⟩ \to 2^{nd} (X) - 1 = y - 1$
186	185	oveq1d	$⊢ X = ⟨0, y⟩ \to (2^{nd} (X) - 1) \mod N = (y - 1) \mod N$
187	186	opeq2d	$⊢ X = ⟨0, y⟩ \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (y - 1) \mod N⟩$
188	174 187	preq12d	$⊢ X = ⟨0, y⟩ \to \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\}$
189	188	eleq1d	$⊢ X = ⟨0, y⟩ \to (\{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} \in E)$
190	181 184 189	3anbi123d	$⊢ X = ⟨0, y⟩ \to ((\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E) \leftrightarrow (\{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \in E \land \{⟨0, y⟩, ⟨1, y⟩\} \in E \land \{⟨0, y⟩, ⟨0, (y - 1) \mod N⟩\} \in E))$
191	173 190	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (X = ⟨0, y⟩ \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E))$
192	191	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land x = 0) \to (X = ⟨0, y⟩ \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E))$
193	16 192	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land x = 0) \to (X = ⟨x, y⟩ \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E))$
194	193	impancom	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land X = ⟨x, y⟩) \to (x = 0 \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E))$
195	13 194	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land X = ⟨x, y⟩) \to (1^{st} (X) = 0 \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E))$
196	195	ex	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (X = ⟨x, y⟩ \to (1^{st} (X) = 0 \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E)))$
197	196	rexlimdvva	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩ \to (1^{st} (X) = 0 \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E)))$
198	6 197	sylbid	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \to (1^{st} (X) = 0 \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E)))$
199	198	imp32	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (\{X, ⟨0, (2^{nd} (X) + 1) \mod N⟩\} \in E \land \{X, ⟨1, 2^{nd} (X)⟩\} \in E \land \{X, ⟨0, (2^{nd} (X) - 1) \mod N⟩\} \in E)$

Metamath Proof Explorer

Theorem gpgedgvtx0

Proof