gpgvtxedg1

Description: The edges starting at a vertex X of the second kind 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	gpgvtxedg1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land \{X, Y\} \in E) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)$

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		gpgusgra	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( \|^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) with typecode \|-
6	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
7	6	anbi2i	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \leftrightarrow (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉))$
8	2	eleq1i	Could not format ( G e. USGraph <-> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for \|- ( G e. USGraph <-> ( N gPetersenGr K ) e. USGraph ) with typecode \|-
9	5 7 8	3imtr4i	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to G \in USGraph$
10	9	3ad2ant1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land \{X, Y\} \in E) \to G \in USGraph$
11		simp3	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land \{X, Y\} \in E) \to \{X, Y\} \in E$
12	4 3	usgrpredgv	$⊢ (G \in USGraph \land \{X, Y\} \in E) \to (X \in V \land Y \in V)$
13	10 11 12	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land \{X, Y\} \in E) \to (X \in V \land Y \in V)$
14		eqid	$⊢ (0 ..^N) = (0 ..^N)$
15	14 1 2 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{X, Y\} \in E \leftrightarrow \exists y \in (0 ..^N) (\{X, Y\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{X, Y\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
16	15	3ad2ant1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \to (\{X, Y\} \in E \leftrightarrow \exists y \in (0 ..^N) (\{X, Y\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{X, Y\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}))$
17		simp3	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \to (X \in V \land Y \in V)$
18	17	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (X \in V \land Y \in V)$
19		opex	$⊢ ⟨0, y⟩ \in V$
20		opex	$⊢ ⟨0, (y + 1) \mod N⟩ \in V$
21	19 20	pm3.2i	$⊢ (⟨0, y⟩ \in V \land ⟨0, (y + 1) \mod N⟩ \in V)$
22		preq12bg	$⊢ ((X \in V \land Y \in V) \land (⟨0, y⟩ \in V \land ⟨0, (y + 1) \mod N⟩ \in V)) \to (\{X, Y\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \leftrightarrow ((X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \lor (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)))$
23	18 21 22	sylancl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (\{X, Y\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \leftrightarrow ((X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \lor (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)))$
24		c0ex	$⊢ 0 \in V$
25		vex	$⊢ y \in V$
26	24 25	op1std	$⊢ X = ⟨0, y⟩ \to 1^{st} (X) = 0$
27	26	eqeq1d	$⊢ X = ⟨0, y⟩ \to (1^{st} (X) = 1 \leftrightarrow 0 = 1)$
28		eqcom	$⊢ 0 = 1 \leftrightarrow 1 = 0$
29	27 28	bitrdi	$⊢ X = ⟨0, y⟩ \to (1^{st} (X) = 1 \leftrightarrow 1 = 0)$
30		ax-1ne0	$⊢ 1 \neq 0$
31		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = ⟨0, (y + 1) \mod N⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
32	31	com12	$⊢ 1 \neq 0 \to (1 = 0 \to (Y = ⟨0, (y + 1) \mod N⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
33	30 32	mp1i	$⊢ X = ⟨0, y⟩ \to (1 = 0 \to (Y = ⟨0, (y + 1) \mod N⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
34	29 33	sylbid	$⊢ X = ⟨0, y⟩ \to (1^{st} (X) = 1 \to (Y = ⟨0, (y + 1) \mod N⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
35	34	com12	$⊢ 1^{st} (X) = 1 \to (X = ⟨0, y⟩ \to (Y = ⟨0, (y + 1) \mod N⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
36	35	impd	$⊢ 1^{st} (X) = 1 \to ((X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
37		ovex	$⊢ (y + 1) \mod N \in V$
38	24 37	op1std	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to 1^{st} (X) = 0$
39	38	eqeq1d	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to (1^{st} (X) = 1 \leftrightarrow 0 = 1)$
40	39 28	bitrdi	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to (1^{st} (X) = 1 \leftrightarrow 1 = 0)$
41		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = ⟨0, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
42	41	com12	$⊢ 1 \neq 0 \to (1 = 0 \to (Y = ⟨0, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
43	30 42	mp1i	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to (1 = 0 \to (Y = ⟨0, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
44	40 43	sylbid	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to (1^{st} (X) = 1 \to (Y = ⟨0, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
45	44	com12	$⊢ 1^{st} (X) = 1 \to (X = ⟨0, (y + 1) \mod N⟩ \to (Y = ⟨0, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
46	45	impd	$⊢ 1^{st} (X) = 1 \to ((X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
47	36 46	jaod	$⊢ 1^{st} (X) = 1 \to (((X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \lor (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
48	47	3ad2ant2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \to (((X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \lor (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
49	48	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (((X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \lor (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
50	23 49	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (\{X, Y\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
51		opex	$⊢ ⟨1, y⟩ \in V$
52	19 51	pm3.2i	$⊢ (⟨0, y⟩ \in V \land ⟨1, y⟩ \in V)$
53		preq12bg	$⊢ ((X \in V \land Y \in V) \land (⟨0, y⟩ \in V \land ⟨1, y⟩ \in V)) \to (\{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \leftrightarrow ((X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \lor (X = ⟨1, y⟩ \land Y = ⟨0, y⟩)))$
54	18 52 53	sylancl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (\{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \leftrightarrow ((X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \lor (X = ⟨1, y⟩ \land Y = ⟨0, y⟩)))$
55		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = ⟨1, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
56	55	com12	$⊢ 1 \neq 0 \to (1 = 0 \to (Y = ⟨1, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
57	30 56	mp1i	$⊢ X = ⟨0, y⟩ \to (1 = 0 \to (Y = ⟨1, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
58	29 57	sylbid	$⊢ X = ⟨0, y⟩ \to (1^{st} (X) = 1 \to (Y = ⟨1, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
59	58	com12	$⊢ 1^{st} (X) = 1 \to (X = ⟨0, y⟩ \to (Y = ⟨1, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
60	59	3ad2ant2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \to (X = ⟨0, y⟩ \to (Y = ⟨1, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
61	60	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (X = ⟨0, y⟩ \to (Y = ⟨1, y⟩ \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)))$
62	61	impd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
63		simpr	$⊢ (X = ⟨1, y⟩ \land Y = ⟨0, y⟩) \to Y = ⟨0, y⟩$
64		1ex	$⊢ 1 \in V$
65	64 25	op2ndd	$⊢ X = ⟨1, y⟩ \to 2^{nd} (X) = y$
66	65	eqcomd	$⊢ X = ⟨1, y⟩ \to y = 2^{nd} (X)$
67	66	adantr	$⊢ (X = ⟨1, y⟩ \land Y = ⟨0, y⟩) \to y = 2^{nd} (X)$
68	67	opeq2d	$⊢ (X = ⟨1, y⟩ \land Y = ⟨0, y⟩) \to ⟨0, y⟩ = ⟨0, 2^{nd} (X)⟩$
69	63 68	eqtrd	$⊢ (X = ⟨1, y⟩ \land Y = ⟨0, y⟩) \to Y = ⟨0, 2^{nd} (X)⟩$
70	69	adantl	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨1, y⟩ \land Y = ⟨0, y⟩)) \to Y = ⟨0, 2^{nd} (X)⟩$
71	70	3mix2d	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨1, y⟩ \land Y = ⟨0, y⟩)) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)$
72	71	ex	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨1, y⟩ \land Y = ⟨0, y⟩) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
73	62 72	jaod	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (((X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \lor (X = ⟨1, y⟩ \land Y = ⟨0, y⟩)) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
74	54 73	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (\{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
75		opex	$⊢ ⟨1, (y + K) \mod N⟩ \in V$
76	51 75	pm3.2i	$⊢ (⟨1, y⟩ \in V \land ⟨1, (y + K) \mod N⟩ \in V)$
77		preq12bg	$⊢ ((X \in V \land Y \in V) \land (⟨1, y⟩ \in V \land ⟨1, (y + K) \mod N⟩ \in V)) \to (\{X, Y\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \leftrightarrow ((X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \lor (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)))$
78	18 76 77	sylancl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (\{X, Y\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \leftrightarrow ((X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \lor (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)))$
79		simpr	$⊢ (X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \to Y = ⟨1, (y + K) \mod N⟩$
80	66	oveq1d	$⊢ X = ⟨1, y⟩ \to y + K = 2^{nd} (X) + K$
81	80	oveq1d	$⊢ X = ⟨1, y⟩ \to (y + K) \mod N = (2^{nd} (X) + K) \mod N$
82	81	adantr	$⊢ (X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \to (y + K) \mod N = (2^{nd} (X) + K) \mod N$
83	82	opeq2d	$⊢ (X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \to ⟨1, (y + K) \mod N⟩ = ⟨1, (2^{nd} (X) + K) \mod N⟩$
84	79 83	eqtrd	$⊢ (X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \to Y = ⟨1, (2^{nd} (X) + K) \mod N⟩$
85	84	3mix1d	$⊢ (X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)$
86	85	a1i	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
87		elfzoelz	$⊢ y \in (0 ..^N) \to y \in ℤ$
88	87	zred	$⊢ y \in (0 ..^N) \to y \in ℝ$
89	88	adantl	$⊢ (K \in J \land y \in (0 ..^N)) \to y \in ℝ$
90		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
91	90	zred	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℝ$
92	6 91	sylbi	$⊢ K \in J \to K \in ℝ$
93	92	adantr	$⊢ (K \in J \land y \in (0 ..^N)) \to K \in ℝ$
94	89 93	readdcld	$⊢ (K \in J \land y \in (0 ..^N)) \to y + K \in ℝ$
95		elfzo0	$⊢ y \in (0 ..^N) \leftrightarrow (y \in ℕ_{0} \land N \in ℕ \land y < N)$
96		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
97	96	3ad2ant2	$⊢ (y \in ℕ_{0} \land N \in ℕ \land y < N) \to N \in ℝ^{+}$
98	95 97	sylbi	$⊢ y \in (0 ..^N) \to N \in ℝ^{+}$
99	98	adantl	$⊢ (K \in J \land y \in (0 ..^N)) \to N \in ℝ^{+}$
100		modsubmod	$⊢ (y + K \in ℝ \land K \in ℝ \land N \in ℝ^{+}) \to (((y + K) \mod N) - K) \mod N = (y + K - K) \mod N$
101	94 93 99 100	syl3anc	$⊢ (K \in J \land y \in (0 ..^N)) \to (((y + K) \mod N) - K) \mod N = (y + K - K) \mod N$
102	87	zcnd	$⊢ y \in (0 ..^N) \to y \in ℂ$
103	102	adantl	$⊢ (K \in J \land y \in (0 ..^N)) \to y \in ℂ$
104	93	recnd	$⊢ (K \in J \land y \in (0 ..^N)) \to K \in ℂ$
105	103 104	pncand	$⊢ (K \in J \land y \in (0 ..^N)) \to y + K - K = y$
106	105	oveq1d	$⊢ (K \in J \land y \in (0 ..^N)) \to (y + K - K) \mod N = y \mod N$
107		zmodidfzoimp	$⊢ y \in (0 ..^N) \to y \mod N = y$
108	107	adantl	$⊢ (K \in J \land y \in (0 ..^N)) \to y \mod N = y$
109	101 106 108	3eqtrrd	$⊢ (K \in J \land y \in (0 ..^N)) \to y = (((y + K) \mod N) - K) \mod N$
110	109	ex	$⊢ K \in J \to (y \in (0 ..^N) \to y = (((y + K) \mod N) - K) \mod N)$
111	110	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (y \in (0 ..^N) \to y = (((y + K) \mod N) - K) \mod N)$
112	111	3ad2ant1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \to (y \in (0 ..^N) \to y = (((y + K) \mod N) - K) \mod N)$
113	112	imp	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to y = (((y + K) \mod N) - K) \mod N$
114	113	adantr	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to y = (((y + K) \mod N) - K) \mod N$
115	114	opeq2d	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to ⟨1, y⟩ = ⟨1, (((y + K) \mod N) - K) \mod N⟩$
116		simpr	$⊢ (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩) \to Y = ⟨1, y⟩$
117		ovex	$⊢ (y + K) \mod N \in V$
118	64 117	op2ndd	$⊢ X = ⟨1, (y + K) \mod N⟩ \to 2^{nd} (X) = (y + K) \mod N$
119	118	oveq1d	$⊢ X = ⟨1, (y + K) \mod N⟩ \to 2^{nd} (X) - K = ((y + K) \mod N) - K$
120	119	oveq1d	$⊢ X = ⟨1, (y + K) \mod N⟩ \to (2^{nd} (X) - K) \mod N = (((y + K) \mod N) - K) \mod N$
121	120	opeq2d	$⊢ X = ⟨1, (y + K) \mod N⟩ \to ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (((y + K) \mod N) - K) \mod N⟩$
122	121	adantr	$⊢ (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩) \to ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (((y + K) \mod N) - K) \mod N⟩$
123	116 122	eqeq12d	$⊢ (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩) \to (Y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \leftrightarrow ⟨1, y⟩ = ⟨1, (((y + K) \mod N) - K) \mod N⟩)$
124	123	adantl	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to (Y = ⟨1, (2^{nd} (X) - K) \mod N⟩ \leftrightarrow ⟨1, y⟩ = ⟨1, (((y + K) \mod N) - K) \mod N⟩)$
125	115 124	mpbird	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to Y = ⟨1, (2^{nd} (X) - K) \mod N⟩$
126	125	3mix3d	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)$
127	126	ex	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
128	86 127	jaod	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (((X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \lor (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
129	78 128	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (\{X, Y\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\} \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
130	50 74 129	3jaod	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((\{X, Y\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{X, Y\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
131	130	rexlimdva	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \to (\exists y \in (0 ..^N) (\{X, Y\} = \{⟨0, y⟩, ⟨0, (y + 1) \mod N⟩\} \lor \{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \lor \{X, Y\} = \{⟨1, y⟩, ⟨1, (y + K) \mod N⟩\}) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
132	16 131	sylbid	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land (X \in V \land Y \in V)) \to (\{X, Y\} \in E \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
133	132	3exp	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (1^{st} (X) = 1 \to ((X \in V \land Y \in V) \to (\{X, Y\} \in E \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))))$
134	133	com34	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (1^{st} (X) = 1 \to (\{X, Y\} \in E \to ((X \in V \land Y \in V) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))))$
135	134	3imp	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land \{X, Y\} \in E) \to ((X \in V \land Y \in V) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩))$
136	13 135	mpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 1 \land \{X, Y\} \in E) \to (Y = ⟨1, (2^{nd} (X) + K) \mod N⟩ \lor Y = ⟨0, 2^{nd} (X)⟩ \lor Y = ⟨1, (2^{nd} (X) - K) \mod N⟩)$

Metamath Proof Explorer

Theorem gpgvtxedg1

Proof