gpgedgvtx1

Description: The edges starting at an inside vertex in a generalized Petersen graph G . (Contributed by AV, 2-Sep-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	gpgedgvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \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) = 1 \leftrightarrow x = 1)$
14		opeq1	$⊢ x = 1 \to ⟨x, y⟩ = ⟨1, y⟩$
15	14	eqeq2d	$⊢ x = 1 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨1, y⟩)$
16	15	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land x = 1) \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨1, y⟩)$
17		opeq2	$⊢ z = y \to ⟨0, z⟩ = ⟨0, y⟩$
18		oveq1	$⊢ z = y \to z + 1 = y + 1$
19	18	oveq1d	$⊢ z = y \to (z + 1) \mod N = (y + 1) \mod N$
20	19	opeq2d	$⊢ z = y \to ⟨0, (z + 1) \mod N⟩ = ⟨0, (y + 1) \mod N⟩$
21	17 20	preq12d	$⊢ z = y \to \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\}$
22	21	eqeq2d	$⊢ z = y \to (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\})$
23		opeq2	$⊢ z = y \to ⟨1, z⟩ = ⟨1, y⟩$
24	17 23	preq12d	$⊢ z = y \to \{⟨0, z⟩, ⟨1, z⟩\} = \{⟨0, y⟩, ⟨1, y⟩\}$
25	24	eqeq2d	$⊢ z = y \to (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\})$
26		oveq1	$⊢ z = y \to z + K = y + K$
27	26	oveq1d	$⊢ z = y \to (z + K) \mod N = (y + K) \mod N$
28	27	opeq2d	$⊢ z = y \to ⟨1, (z + K) \mod N⟩ = ⟨1, (y + K) \mod N⟩$
29	23 28	preq12d	$⊢ z = y \to \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}$
30	29	eqeq2d	$⊢ z = y \to (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
31	22 25 30	3orbi123d	$⊢ z = y \to ((\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
32		simpr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to y \in (0 ..^N)$
33		eqid	$⊢ \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}$
34	33	3mix3i	$⊢ (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
35	34	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
36	31 32 35	rspcedvdw	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
37	21	eqeq2d	$⊢ z = y \to (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\})$
38	24	eqeq2d	$⊢ z = y \to (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\})$
39	29	eqeq2d	$⊢ z = y \to (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
40	37 38 39	3orbi123d	$⊢ z = y \to ((\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
41		prcom	$⊢ \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\}$
42	41	3mix2i	$⊢ (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
43	42	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\})$
44	40 32 43	rspcedvdw	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
45		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
46	45 1	eleq2s	$⊢ K \in J \to K \in ℤ$
47	46	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \in ℤ$
48	47	anim1ci	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (y \in (0 ..^N) \land K \in ℤ)$
49		fzospliti	$⊢ (y \in (0 ..^N) \land K \in ℤ) \to (y \in (0 ..^K) \lor y \in (K ..^N))$
50	48 49	syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (y \in (0 ..^K) \lor y \in (K ..^N))$
51	50	ex	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (y \in (0 ..^N) \to (y \in (0 ..^K) \lor y \in (K ..^N)))$
52		opeq2	$⊢ z = N + y - K \to ⟨0, z⟩ = ⟨0, N + y - K⟩$
53		oveq1	$⊢ z = N + y - K \to z + 1 = (N + y) - K + 1$
54	53	oveq1d	$⊢ z = N + y - K \to (z + 1) \mod N = ((N + y) - K + 1) \mod N$
55	54	opeq2d	$⊢ z = N + y - K \to ⟨0, (z + 1) \mod N⟩ = ⟨0, ((N + y) - K + 1) \mod N⟩$
56	52 55	preq12d	$⊢ z = N + y - K \to \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} = \{⟨0, N + y - K⟩, ⟨0, ((N + y) - K + 1) \mod N⟩\}$
57	56	eqeq2d	$⊢ z = N + y - K \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, N + y - K⟩, ⟨0, ((N + y) - K + 1) \mod N⟩\})$
58		opeq2	$⊢ z = N + y - K \to ⟨1, z⟩ = ⟨1, N + y - K⟩$
59	52 58	preq12d	$⊢ z = N + y - K \to \{⟨0, z⟩, ⟨1, z⟩\} = \{⟨0, N + y - K⟩, ⟨1, N + y - K⟩\}$
60	59	eqeq2d	$⊢ z = N + y - K \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, N + y - K⟩, ⟨1, N + y - K⟩\})$
61		oveq1	$⊢ z = N + y - K \to z + K = (N + y) - K + K$
62	61	oveq1d	$⊢ z = N + y - K \to (z + K) \mod N = ((N + y) - K + K) \mod N$
63	62	opeq2d	$⊢ z = N + y - K \to ⟨1, (z + K) \mod N⟩ = ⟨1, ((N + y) - K + K) \mod N⟩$
64	58 63	preq12d	$⊢ z = N + y - K \to \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} = \{⟨1, N + y - K⟩, ⟨1, ((N + y) - K + K) \mod N⟩\}$
65	64	eqeq2d	$⊢ z = N + y - K \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, N + y - K⟩, ⟨1, ((N + y) - K + K) \mod N⟩\})$
66	57 60 65	3orbi123d	$⊢ z = N + y - K \to ((\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, N + y - K⟩, ⟨0, ((N + y) - K + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, N + y - K⟩, ⟨1, N + y - K⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, N + y - K⟩, ⟨1, ((N + y) - K + K) \mod N⟩\}))$
67		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
68	67	nnzd	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
69	68	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℤ$
70	69	zcnd	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℂ$
71	70	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N \in ℂ$
72		elfzoel2	$⊢ y \in (0 ..^K) \to K \in ℤ$
73	72	zcnd	$⊢ y \in (0 ..^K) \to K \in ℂ$
74	73	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K \in ℂ$
75		elfzoelz	$⊢ y \in (0 ..^K) \to y \in ℤ$
76	75	zcnd	$⊢ y \in (0 ..^K) \to y \in ℂ$
77	76	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to y \in ℂ$
78	71 74 77	subsub3d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N - (K - y) = N + y - K$
79		1zzd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to 1 \in ℤ$
80	69	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N \in ℤ$
81	72	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K \in ℤ$
82	75	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to y \in ℤ$
83	81 82	zsubcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K - y \in ℤ$
84		elfzo0subge1	$⊢ y \in (0 ..^K) \to 1 \leq K - y$
85	84	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to 1 \leq K - y$
86	83	zred	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K - y \in ℝ$
87	81	zred	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K \in ℝ$
88	80	zred	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N \in ℝ$
89		elfzo0suble	$⊢ y \in (0 ..^K) \to K - y \leq K$
90	89	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K - y \leq K$
91	1 5	gpgedgvtx1lem	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \in (0 ..^N)$
92		elfzo0le	$⊢ K \in (0 ..^N) \to K \leq N$
93	91 92	syl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \leq N$
94	93	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K \leq N$
95	86 87 88 90 94	letrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K - y \leq N$
96	79 80 83 85 95	elfzd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K - y \in (1 \dots N)$
97		ubmelfzo	$⊢ K - y \in (1 \dots N) \to N - (K - y) \in (0 ..^N)$
98	96 97	syl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N - (K - y) \in (0 ..^N)$
99	78 98	eqeltrrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N + y - K \in (0 ..^N)$
100		eluzelcn	$⊢ N \in ℤ_{\geq 3} \to N \in ℂ$
101	100	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℂ$
102	101	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N \in ℂ$
103	102 77	addcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N + y \in ℂ$
104	103 74	npcand	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to (N + y) - K + K = N + y$
105	104	oveq1d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to ((N + y) - K + K) \mod N = (N + y) \mod N$
106		elfzonn0	$⊢ y \in (0 ..^K) \to y \in ℕ_{0}$
107	106	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to y \in ℕ_{0}$
108	67	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℕ$
109	108	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to N \in ℕ$
110		elfzouz2	$⊢ K \in (0 ..^N) \to N \in ℤ_{\geq K}$
111		fzoss2	$⊢ N \in ℤ_{\geq K} \to (0 ..^K) \subseteq (0 ..^N)$
112	110 111	syl	$⊢ K \in (0 ..^N) \to (0 ..^K) \subseteq (0 ..^N)$
113	112	sseld	$⊢ K \in (0 ..^N) \to (y \in (0 ..^K) \to y \in (0 ..^N))$
114		elfzolt2	$⊢ y \in (0 ..^N) \to y < N$
115	113 114	syl6	$⊢ K \in (0 ..^N) \to (y \in (0 ..^K) \to y < N)$
116	91 115	syl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (y \in (0 ..^K) \to y < N)$
117	116	imp	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to y < N$
118		addmodid	$⊢ (y \in ℕ_{0} \land N \in ℕ \land y < N) \to (N + y) \mod N = y$
119	107 109 117 118	syl3anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to (N + y) \mod N = y$
120	105 119	eqtr2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to y = ((N + y) - K + K) \mod N$
121	120	opeq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to ⟨1, y⟩ = ⟨1, ((N + y) - K + K) \mod N⟩$
122		simpr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to y \in (0 ..^K)$
123		elfzolt2	$⊢ K \in (0 ..^N) \to K < N$
124	91 123	syl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K < N$
125	124	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to K < N$
126		submodlt	$⊢ (N \in ℕ \land y \in (0 ..^K) \land K < N) \to (y - K) \mod N = N + y - K$
127	109 122 125 126	syl3anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to (y - K) \mod N = N + y - K$
128	127	opeq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to ⟨1, (y - K) \mod N⟩ = ⟨1, N + y - K⟩$
129	121 128	preq12d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, ((N + y) - K + K) \mod N⟩, ⟨1, N + y - K⟩\}$
130		prcom	$⊢ \{⟨1, ((N + y) - K + K) \mod N⟩, ⟨1, N + y - K⟩\} = \{⟨1, N + y - K⟩, ⟨1, ((N + y) - K + K) \mod N⟩\}$
131	129 130	eqtrdi	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, N + y - K⟩, ⟨1, ((N + y) - K + K) \mod N⟩\}$
132	131	3mix3d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, N + y - K⟩, ⟨0, ((N + y) - K + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, N + y - K⟩, ⟨1, N + y - K⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, N + y - K⟩, ⟨1, ((N + y) - K + K) \mod N⟩\})$
133	66 99 132	rspcedvdw	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^K)) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
134	133	ex	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (y \in (0 ..^K) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
135		opeq2	$⊢ z = y - K \to ⟨0, z⟩ = ⟨0, y - K⟩$
136		oveq1	$⊢ z = y - K \to z + 1 = y - K + 1$
137	136	oveq1d	$⊢ z = y - K \to (z + 1) \mod N = (y - K + 1) \mod N$
138	137	opeq2d	$⊢ z = y - K \to ⟨0, (z + 1) \mod N⟩ = ⟨0, (y - K + 1) \mod N⟩$
139	135 138	preq12d	$⊢ z = y - K \to \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} = \{⟨0, y - K⟩, ⟨0, (y - K + 1) \mod N⟩\}$
140	139	eqeq2d	$⊢ z = y - K \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, y - K⟩, ⟨0, (y - K + 1) \mod N⟩\})$
141		opeq2	$⊢ z = y - K \to ⟨1, z⟩ = ⟨1, y - K⟩$
142	135 141	preq12d	$⊢ z = y - K \to \{⟨0, z⟩, ⟨1, z⟩\} = \{⟨0, y - K⟩, ⟨1, y - K⟩\}$
143	142	eqeq2d	$⊢ z = y - K \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, y - K⟩, ⟨1, y - K⟩\})$
144		oveq1	$⊢ z = y - K \to z + K = y - K + K$
145	144	oveq1d	$⊢ z = y - K \to (z + K) \mod N = (y - K + K) \mod N$
146	145	opeq2d	$⊢ z = y - K \to ⟨1, (z + K) \mod N⟩ = ⟨1, (y - K + K) \mod N⟩$
147	141 146	preq12d	$⊢ z = y - K \to \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} = \{⟨1, y - K⟩, ⟨1, (y - K + K) \mod N⟩\}$
148	147	eqeq2d	$⊢ z = y - K \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\} \leftrightarrow \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, y - K⟩, ⟨1, (y - K + K) \mod N⟩\})$
149	140 143 148	3orbi123d	$⊢ z = y - K \to ((\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \leftrightarrow (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, y - K⟩, ⟨0, (y - K + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, y - K⟩, ⟨1, y - K⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, y - K⟩, ⟨1, (y - K + K) \mod N⟩\}))$
150		elfzo1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉)$
151	150	simp1bi	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℕ$
152	151	nnnn0d	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℕ_{0}$
153	152 1	eleq2s	$⊢ K \in J \to K \in ℕ_{0}$
154	153	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \in ℕ_{0}$
155		elfzoextl	$⊢ (y \in (K ..^N) \land K \in ℕ_{0}) \to y \in (K ..^K + N)$
156	154 155	sylan2	$⊢ (y \in (K ..^N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to y \in (K ..^K + N)$
157	156	ancoms	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to y \in (K ..^K + N)$
158	108	nnzd	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℤ$
159	158	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to N \in ℤ$
160		fzosubel3	$⊢ (y \in (K ..^K + N) \land N \in ℤ) \to y - K \in (0 ..^N)$
161	157 159 160	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to y - K \in (0 ..^N)$
162		elfzoelz	$⊢ y \in (K ..^N) \to y \in ℤ$
163	162	zcnd	$⊢ y \in (K ..^N) \to y \in ℂ$
164		elfzoel1	$⊢ y \in (K ..^N) \to K \in ℤ$
165	164	zcnd	$⊢ y \in (K ..^N) \to K \in ℂ$
166	163 165	npcand	$⊢ y \in (K ..^N) \to y - K + K = y$
167	166	oveq1d	$⊢ y \in (K ..^N) \to (y - K + K) \mod N = y \mod N$
168	167	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to (y - K + K) \mod N = y \mod N$
169	67	nnrpd	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ^{+}$
170	169	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℝ^{+}$
171	162	zred	$⊢ y \in (K ..^N) \to y \in ℝ$
172	170 171	anim12ci	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to (y \in ℝ \land N \in ℝ^{+})$
173		elfzole1	$⊢ y \in (K ..^N) \to K \leq y$
174	173	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to K \leq y$
175		0red	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \land K \leq y) \to 0 \in ℝ$
176	164	zred	$⊢ y \in (K ..^N) \to K \in ℝ$
177	176	ad2antlr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \land K \leq y) \to K \in ℝ$
178	171	ad2antlr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \land K \leq y) \to y \in ℝ$
179		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
180	179	nn0ge0d	$⊢ K \in ℕ \to 0 \leq K$
181	151 180	syl	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 0 \leq K$
182	181 1	eleq2s	$⊢ K \in J \to 0 \leq K$
183	182	ad3antlr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \land K \leq y) \to 0 \leq K$
184		simpr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \land K \leq y) \to K \leq y$
185	175 177 178 183 184	letrd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \land K \leq y) \to 0 \leq y$
186	174 185	mpdan	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to 0 \leq y$
187		elfzolt2	$⊢ y \in (K ..^N) \to y < N$
188	187	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to y < N$
189		modid	$⊢ ((y \in ℝ \land N \in ℝ^{+}) \land (0 \leq y \land y < N)) \to y \mod N = y$
190	172 186 188 189	syl12anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to y \mod N = y$
191	168 190	eqtr2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to y = (y - K + K) \mod N$
192	191	opeq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to ⟨1, y⟩ = ⟨1, (y - K + K) \mod N⟩$
193	171 176	resubcld	$⊢ y \in (K ..^N) \to y - K \in ℝ$
194	170 193	anim12ci	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to (y - K \in ℝ \land N \in ℝ^{+})$
195		elfzo2	$⊢ y \in (K ..^N) \leftrightarrow (y \in ℤ_{\geq K} \land N \in ℤ \land y < N)$
196		eluz2	$⊢ y \in ℤ_{\geq K} \leftrightarrow (K \in ℤ \land y \in ℤ \land K \leq y)$
197		simp13	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to K \leq y$
198		zre	$⊢ K \in ℤ \to K \in ℝ$
199		zre	$⊢ y \in ℤ \to y \in ℝ$
200	198 199	anim12ci	$⊢ (K \in ℤ \land y \in ℤ) \to (y \in ℝ \land K \in ℝ)$
201	200	3adant3	$⊢ (K \in ℤ \land y \in ℤ \land K \leq y) \to (y \in ℝ \land K \in ℝ)$
202	201	3ad2ant1	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to (y \in ℝ \land K \in ℝ)$
203		subge0	$⊢ (y \in ℝ \land K \in ℝ) \to (0 \leq y - K \leftrightarrow K \leq y)$
204	202 203	syl	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to (0 \leq y - K \leftrightarrow K \leq y)$
205	197 204	mpbird	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to 0 \leq y - K$
206	199	3ad2ant2	$⊢ (K \in ℤ \land y \in ℤ \land K \leq y) \to y \in ℝ$
207	206	3ad2ant1	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to y \in ℝ$
208	198	3ad2ant1	$⊢ (K \in ℤ \land y \in ℤ \land K \leq y) \to K \in ℝ$
209	208	3ad2ant1	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to K \in ℝ$
210	207 209	resubcld	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to y - K \in ℝ$
211		zre	$⊢ N \in ℤ \to N \in ℝ$
212	211	adantr	$⊢ (N \in ℤ \land y < N) \to N \in ℝ$
213	212	3ad2ant2	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to N \in ℝ$
214		nnrp	$⊢ K \in ℕ \to K \in ℝ^{+}$
215	214	3ad2ant1	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉) \to K \in ℝ^{+}$
216	150 215	sylbi	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℝ^{+}$
217	216 1	eleq2s	$⊢ K \in J \to K \in ℝ^{+}$
218	217	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \in ℝ^{+}$
219	218	3ad2ant3	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to K \in ℝ^{+}$
220	207 219	ltsubrpd	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to y - K < y$
221		simp2r	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to y < N$
222	210 207 213 220 221	lttrd	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to y - K < N$
223	205 222	jca	$⊢ ((K \in ℤ \land y \in ℤ \land K \leq y) \land (N \in ℤ \land y < N) \land (N \in ℤ_{\geq 3} \land K \in J)) \to (0 \leq y - K \land y - K < N)$
224	223	3exp	$⊢ (K \in ℤ \land y \in ℤ \land K \leq y) \to ((N \in ℤ \land y < N) \to ((N \in ℤ_{\geq 3} \land K \in J) \to (0 \leq y - K \land y - K < N)))$
225	224	expd	$⊢ (K \in ℤ \land y \in ℤ \land K \leq y) \to (N \in ℤ \to (y < N \to ((N \in ℤ_{\geq 3} \land K \in J) \to (0 \leq y - K \land y - K < N))))$
226	196 225	sylbi	$⊢ y \in ℤ_{\geq K} \to (N \in ℤ \to (y < N \to ((N \in ℤ_{\geq 3} \land K \in J) \to (0 \leq y - K \land y - K < N))))$
227	226	3imp	$⊢ (y \in ℤ_{\geq K} \land N \in ℤ \land y < N) \to ((N \in ℤ_{\geq 3} \land K \in J) \to (0 \leq y - K \land y - K < N))$
228	195 227	sylbi	$⊢ y \in (K ..^N) \to ((N \in ℤ_{\geq 3} \land K \in J) \to (0 \leq y - K \land y - K < N))$
229	228	impcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to (0 \leq y - K \land y - K < N)$
230		modid	$⊢ ((y - K \in ℝ \land N \in ℝ^{+}) \land (0 \leq y - K \land y - K < N)) \to (y - K) \mod N = y - K$
231	194 229 230	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to (y - K) \mod N = y - K$
232	231	opeq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to ⟨1, (y - K) \mod N⟩ = ⟨1, y - K⟩$
233	192 232	preq12d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, (y - K + K) \mod N⟩, ⟨1, y - K⟩\}$
234		prcom	$⊢ \{⟨1, (y - K + K) \mod N⟩, ⟨1, y - K⟩\} = \{⟨1, y - K⟩, ⟨1, (y - K + K) \mod N⟩\}$
235	233 234	eqtrdi	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, y - K⟩, ⟨1, (y - K + K) \mod N⟩\}$
236	235	3mix3d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, y - K⟩, ⟨0, (y - K + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, y - K⟩, ⟨1, y - K⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, y - K⟩, ⟨1, (y - K + K) \mod N⟩\})$
237	149 161 236	rspcedvdw	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (K ..^N)) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
238	237	ex	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (y \in (K ..^N) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
239	134 238	jaod	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to ((y \in (0 ..^K) \lor y \in (K ..^N)) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
240	51 239	syld	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (y \in (0 ..^N) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
241	240	imp	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})$
242	5 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \in E \leftrightarrow \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
243	5 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨1, y⟩, ⟨0, y⟩\} \in E \leftrightarrow \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
244	5 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} \in E \leftrightarrow \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}))$
245	242 243 244	3anbi123d	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to ((\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \in E \land \{⟨1, y⟩, ⟨0, y⟩\} \in E \land \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} \in E) \leftrightarrow (\exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})))$
246	245	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to ((\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \in E \land \{⟨1, y⟩, ⟨0, y⟩\} \in E \land \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} \in E) \leftrightarrow (\exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨0, y⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\}) \land \exists z \in (0 ..^N) (\{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨0, (z + 1) \mod N⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨0, z⟩, ⟨1, z⟩\} \lor \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} = \{⟨1, z⟩, ⟨1, (z + K) \mod N⟩\})))$
247	36 44 241 246	mpbir3and	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land y \in (0 ..^N)) \to (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \in E \land \{⟨1, y⟩, ⟨0, y⟩\} \in E \land \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} \in E)$
248	247	adantrl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \in E \land \{⟨1, y⟩, ⟨0, y⟩\} \in E \land \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} \in E)$
249		id	$⊢ X = ⟨1, y⟩ \to X = ⟨1, y⟩$
250		1ex	$⊢ 1 \in V$
251	250 10	op2ndd	$⊢ X = ⟨1, y⟩ \to 2^{nd} (X) = y$
252	251	oveq1d	$⊢ X = ⟨1, y⟩ \to 2^{nd} (X) + K = y + K$
253	252	oveq1d	$⊢ X = ⟨1, y⟩ \to (2^{nd} (X) + K) \mod N = (y + K) \mod N$
254	253	opeq2d	$⊢ X = ⟨1, y⟩ \to ⟨1, (2^{nd} (X) + K) \mod N⟩ = ⟨1, (y + K) \mod N⟩$
255	249 254	preq12d	$⊢ X = ⟨1, y⟩ \to \{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}$
256	255	eleq1d	$⊢ X = ⟨1, y⟩ \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \leftrightarrow \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \in E)$
257	251	opeq2d	$⊢ X = ⟨1, y⟩ \to ⟨0, 2^{nd} (X)⟩ = ⟨0, y⟩$
258	249 257	preq12d	$⊢ X = ⟨1, y⟩ \to \{X, ⟨0, 2^{nd} (X)⟩\} = \{⟨1, y⟩, ⟨0, y⟩\}$
259	258	eleq1d	$⊢ X = ⟨1, y⟩ \to (\{X, ⟨0, 2^{nd} (X)⟩\} \in E \leftrightarrow \{⟨1, y⟩, ⟨0, y⟩\} \in E)$
260	251	oveq1d	$⊢ X = ⟨1, y⟩ \to 2^{nd} (X) - K = y - K$
261	260	oveq1d	$⊢ X = ⟨1, y⟩ \to (2^{nd} (X) - K) \mod N = (y - K) \mod N$
262	261	opeq2d	$⊢ X = ⟨1, y⟩ \to ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (y - K) \mod N⟩$
263	249 262	preq12d	$⊢ X = ⟨1, y⟩ \to \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} = \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\}$
264	263	eleq1d	$⊢ X = ⟨1, y⟩ \to (\{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E \leftrightarrow \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} \in E)$
265	256 259 264	3anbi123d	$⊢ X = ⟨1, y⟩ \to ((\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E) \leftrightarrow (\{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \in E \land \{⟨1, y⟩, ⟨0, y⟩\} \in E \land \{⟨1, y⟩, ⟨1, (y - K) \mod N⟩\} \in E))$
266	248 265	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (X = ⟨1, y⟩ \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E))$
267	266	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land x = 1) \to (X = ⟨1, y⟩ \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E))$
268	16 267	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land x = 1) \to (X = ⟨x, y⟩ \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E))$
269	268	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 = 1 \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E))$
270	13 269	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) = 1 \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E))$
271	270	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) = 1 \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E)))$
272	271	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) = 1 \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E)))$
273	6 272	sylbid	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \to (1^{st} (X) = 1 \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E)))$
274	273	imp32	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 1)) \to (\{X, ⟨1, (2^{nd} (X) + K) \mod N⟩\} \in E \land \{X, ⟨0, 2^{nd} (X)⟩\} \in E \land \{X, ⟨1, (2^{nd} (X) - K) \mod N⟩\} \in E)$

Metamath Proof Explorer

Theorem gpgedgvtx1

Proof