gpgvtxedg0

Description: The edges starting at a vertex X of the first kind in a generalized Petersen graph G . (Contributed by AV, 30-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	gpgvtxedg0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land \{X, Y\} \in E) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \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) = 0 \land \{X, Y\} \in E) \to G \in USGraph$
11		simp3	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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) = 0 \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) = 0 \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) = 0 \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) = 0 \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) = 0 \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		simpr	$⊢ (X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \to Y = ⟨0, (y + 1) \mod N⟩$
25		c0ex	$⊢ 0 \in V$
26		vex	$⊢ y \in V$
27	25 26	op2ndd	$⊢ X = ⟨0, y⟩ \to 2^{nd} (X) = y$
28	27	eqcomd	$⊢ X = ⟨0, y⟩ \to y = 2^{nd} (X)$
29	28	oveq1d	$⊢ X = ⟨0, y⟩ \to y + 1 = 2^{nd} (X) + 1$
30	29	oveq1d	$⊢ X = ⟨0, y⟩ \to (y + 1) \mod N = (2^{nd} (X) + 1) \mod N$
31	30	adantr	$⊢ (X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \to (y + 1) \mod N = (2^{nd} (X) + 1) \mod N$
32	31	opeq2d	$⊢ (X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \to ⟨0, (y + 1) \mod N⟩ = ⟨0, (2^{nd} (X) + 1) \mod N⟩$
33	24 32	eqtrd	$⊢ (X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \to Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩$
34	33	3mix1d	$⊢ (X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
35	34	a1i	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨0, y⟩ \land Y = ⟨0, (y + 1) \mod N⟩) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
36		elfzoelz	$⊢ y \in (0 ..^N) \to y \in ℤ$
37	36	zred	$⊢ y \in (0 ..^N) \to y \in ℝ$
38		1red	$⊢ y \in (0 ..^N) \to 1 \in ℝ$
39	37 38	readdcld	$⊢ y \in (0 ..^N) \to y + 1 \in ℝ$
40		elfzo0	$⊢ y \in (0 ..^N) \leftrightarrow (y \in ℕ_{0} \land N \in ℕ \land y < N)$
41		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
42	41	3ad2ant2	$⊢ (y \in ℕ_{0} \land N \in ℕ \land y < N) \to N \in ℝ^{+}$
43	40 42	sylbi	$⊢ y \in (0 ..^N) \to N \in ℝ^{+}$
44		modsubmod	$⊢ (y + 1 \in ℝ \land 1 \in ℝ \land N \in ℝ^{+}) \to (((y + 1) \mod N) - 1) \mod N = (y + 1 - 1) \mod N$
45	39 38 43 44	syl3anc	$⊢ y \in (0 ..^N) \to (((y + 1) \mod N) - 1) \mod N = (y + 1 - 1) \mod N$
46	36	zcnd	$⊢ y \in (0 ..^N) \to y \in ℂ$
47		pncan1	$⊢ y \in ℂ \to y + 1 - 1 = y$
48	46 47	syl	$⊢ y \in (0 ..^N) \to y + 1 - 1 = y$
49	48	oveq1d	$⊢ y \in (0 ..^N) \to (y + 1 - 1) \mod N = y \mod N$
50		zmodidfzoimp	$⊢ y \in (0 ..^N) \to y \mod N = y$
51	45 49 50	3eqtrrd	$⊢ y \in (0 ..^N) \to y = (((y + 1) \mod N) - 1) \mod N$
52	51	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to y = (((y + 1) \mod N) - 1) \mod N$
53	52	adantr	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to y = (((y + 1) \mod N) - 1) \mod N$
54	53	opeq2d	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to ⟨0, y⟩ = ⟨0, (((y + 1) \mod N) - 1) \mod N⟩$
55		simpr	$⊢ (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩) \to Y = ⟨0, y⟩$
56		ovex	$⊢ (y + 1) \mod N \in V$
57	25 56	op2ndd	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to 2^{nd} (X) = (y + 1) \mod N$
58	57	oveq1d	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to 2^{nd} (X) - 1 = ((y + 1) \mod N) - 1$
59	58	oveq1d	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to (2^{nd} (X) - 1) \mod N = (((y + 1) \mod N) - 1) \mod N$
60	59	opeq2d	$⊢ X = ⟨0, (y + 1) \mod N⟩ \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (((y + 1) \mod N) - 1) \mod N⟩$
61	60	adantr	$⊢ (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩) \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (((y + 1) \mod N) - 1) \mod N⟩$
62	55 61	eqeq12d	$⊢ (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩) \to (Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \leftrightarrow ⟨0, y⟩ = ⟨0, (((y + 1) \mod N) - 1) \mod N⟩)$
63	62	adantl	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to (Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩ \leftrightarrow ⟨0, y⟩ = ⟨0, (((y + 1) \mod N) - 1) \mod N⟩)$
64	54 63	mpbird	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩$
65	64	3mix3d	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩)) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
66	65	ex	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨0, (y + 1) \mod N⟩ \land Y = ⟨0, y⟩) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
67	35 66	jaod	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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 = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
68	23 67	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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 = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
69		opex	$⊢ ⟨1, y⟩ \in V$
70	19 69	pm3.2i	$⊢ (⟨0, y⟩ \in V \land ⟨1, y⟩ \in V)$
71		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⟩)))$
72	18 70 71	sylancl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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⟩)))$
73		simpr	$⊢ (X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \to Y = ⟨1, y⟩$
74	28	adantr	$⊢ (X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \to y = 2^{nd} (X)$
75	74	opeq2d	$⊢ (X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \to ⟨1, y⟩ = ⟨1, 2^{nd} (X)⟩$
76	73 75	eqtrd	$⊢ (X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \to Y = ⟨1, 2^{nd} (X)⟩$
77	76	adantl	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨0, y⟩ \land Y = ⟨1, y⟩)) \to Y = ⟨1, 2^{nd} (X)⟩$
78	77	3mix2d	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \land (X = ⟨0, y⟩ \land Y = ⟨1, y⟩)) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$
79	78	ex	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨0, y⟩ \land Y = ⟨1, y⟩) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
80		1ex	$⊢ 1 \in V$
81	80 26	op1std	$⊢ X = ⟨1, y⟩ \to 1^{st} (X) = 1$
82	81	eqeq1d	$⊢ X = ⟨1, y⟩ \to (1^{st} (X) = 0 \leftrightarrow 1 = 0)$
83		ax-1ne0	$⊢ 1 \neq 0$
84		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = ⟨0, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
85	84	com12	$⊢ 1 \neq 0 \to (1 = 0 \to (Y = ⟨0, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
86	83 85	mp1i	$⊢ X = ⟨1, y⟩ \to (1 = 0 \to (Y = ⟨0, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
87	82 86	sylbid	$⊢ X = ⟨1, y⟩ \to (1^{st} (X) = 0 \to (Y = ⟨0, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
88	87	com12	$⊢ 1^{st} (X) = 0 \to (X = ⟨1, y⟩ \to (Y = ⟨0, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
89	88	3ad2ant2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \to (X = ⟨1, y⟩ \to (Y = ⟨0, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
90	89	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (X = ⟨1, y⟩ \to (Y = ⟨0, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
91	90	impd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to ((X = ⟨1, y⟩ \land Y = ⟨0, y⟩) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
92	79 91	jaod	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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 = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
93	72 92	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \land y \in (0 ..^N)) \to (\{X, Y\} = \{⟨0, y⟩, ⟨1, y⟩\} \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
94		opex	$⊢ ⟨1, (y + K) \mod N⟩ \in V$
95	69 94	pm3.2i	$⊢ (⟨1, y⟩ \in V \land ⟨1, (y + K) \mod N⟩ \in V)$
96		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⟩)))$
97	18 95 96	sylancl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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⟩)))$
98		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = ⟨1, (y + K) \mod N⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
99	98	com12	$⊢ 1 \neq 0 \to (1 = 0 \to (Y = ⟨1, (y + K) \mod N⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
100	83 99	mp1i	$⊢ X = ⟨1, y⟩ \to (1 = 0 \to (Y = ⟨1, (y + K) \mod N⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
101	82 100	sylbid	$⊢ X = ⟨1, y⟩ \to (1^{st} (X) = 0 \to (Y = ⟨1, (y + K) \mod N⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
102	101	com12	$⊢ 1^{st} (X) = 0 \to (X = ⟨1, y⟩ \to (Y = ⟨1, (y + K) \mod N⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
103	102	impd	$⊢ 1^{st} (X) = 0 \to ((X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
104		ovex	$⊢ (y + K) \mod N \in V$
105	80 104	op1std	$⊢ X = ⟨1, (y + K) \mod N⟩ \to 1^{st} (X) = 1$
106	105	eqeq1d	$⊢ X = ⟨1, (y + K) \mod N⟩ \to (1^{st} (X) = 0 \leftrightarrow 1 = 0)$
107		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = ⟨1, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
108	107	com12	$⊢ 1 \neq 0 \to (1 = 0 \to (Y = ⟨1, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
109	83 108	mp1i	$⊢ X = ⟨1, (y + K) \mod N⟩ \to (1 = 0 \to (Y = ⟨1, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
110	106 109	sylbid	$⊢ X = ⟨1, (y + K) \mod N⟩ \to (1^{st} (X) = 0 \to (Y = ⟨1, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
111	110	com12	$⊢ 1^{st} (X) = 0 \to (X = ⟨1, (y + K) \mod N⟩ \to (Y = ⟨1, y⟩ \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)))$
112	111	impd	$⊢ 1^{st} (X) = 0 \to ((X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
113	103 112	jaod	$⊢ 1^{st} (X) = 0 \to (((X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \lor (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
114	113	3ad2ant2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \to (((X = ⟨1, y⟩ \land Y = ⟨1, (y + K) \mod N⟩) \lor (X = ⟨1, (y + K) \mod N⟩ \land Y = ⟨1, y⟩)) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
115	114	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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 = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
116	97 115	sylbid	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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 = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
117	68 93 116	3jaod	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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 = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
118	117	rexlimdva	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \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 = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
119	16 118	sylbid	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land (X \in V \land Y \in V)) \to (\{X, Y\} \in E \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
120	119	3exp	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (1^{st} (X) = 0 \to ((X \in V \land Y \in V) \to (\{X, Y\} \in E \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))))$
121	120	com34	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (1^{st} (X) = 0 \to (\{X, Y\} \in E \to ((X \in V \land Y \in V) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))))$
122	121	3imp	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land \{X, Y\} \in E) \to ((X \in V \land Y \in V) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩))$
123	13 122	mpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (X) = 0 \land \{X, Y\} \in E) \to (Y = ⟨0, (2^{nd} (X) + 1) \mod N⟩ \lor Y = ⟨1, 2^{nd} (X)⟩ \lor Y = ⟨0, (2^{nd} (X) - 1) \mod N⟩)$

Metamath Proof Explorer

Theorem gpgvtxedg0

Proof