gpgedgiov

Description: The edges of the generalized Petersen graph GPG(N,K) between an inside and an outside vertex. (Contributed by AV, 11-Nov-2025)

	Ref	Expression
Hypotheses	gpgedgiov.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgedgiov.i	$⊢ I = (0 ..^N)$
	gpgedgiov.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpgedgiov.e	$⊢ E = Edg (G)$
Assertion	gpgedgiov	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, X⟩, ⟨1, Y⟩\} \in E \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		gpgedgiov.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgedgiov.i	$⊢ I = (0 ..^N)$
3		gpgedgiov.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
4		gpgedgiov.e	$⊢ E = Edg (G)$
5		simpll	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨1, Y⟩\} \in E) \to (N \in ℤ_{\geq 3} \land K \in J)$
6		c0ex	$⊢ 0 \in V$
7	6	a1i	$⊢ Y \in I \to 0 \in V$
8	7	anim1i	$⊢ (Y \in I \land X \in I) \to (0 \in V \land X \in I)$
9	8	ancoms	$⊢ (X \in I \land Y \in I) \to (0 \in V \land X \in I)$
10		op1stg	$⊢ (0 \in V \land X \in I) \to 1^{st} (⟨0, X⟩) = 0$
11	9 10	syl	$⊢ (X \in I \land Y \in I) \to 1^{st} (⟨0, X⟩) = 0$
12	11	ad2antlr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨1, Y⟩\} \in E) \to 1^{st} (⟨0, X⟩) = 0$
13		simpr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨1, Y⟩\} \in E) \to \{⟨0, X⟩, ⟨1, Y⟩\} \in E$
14		eqid	$⊢ Vtx (G) = Vtx (G)$
15	1 3 14 4	gpgvtxedg0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land 1^{st} (⟨0, X⟩) = 0 \land \{⟨0, X⟩, ⟨1, Y⟩\} \in E) \to (⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩)$
16	5 12 13 15	syl3anc	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land \{⟨0, X⟩, ⟨1, Y⟩\} \in E) \to (⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩)$
17	16	ex	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, X⟩, ⟨1, Y⟩\} \in E \to (⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩))$
18		ovex	$⊢ (X + 1) \mod N \in V$
19	6 18	pm3.2i	$⊢ (0 \in V \land (X + 1) \mod N \in V)$
20		opthg2	$⊢ (0 \in V \land (X + 1) \mod N \in V) \to (⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩ \leftrightarrow (1 = 0 \land Y = (X + 1) \mod N))$
21	19 20	mp1i	$⊢ (X \in I \land Y \in I) \to (⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩ \leftrightarrow (1 = 0 \land Y = (X + 1) \mod N))$
22		ax-1ne0	$⊢ 1 \neq 0$
23		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = (X + 1) \mod N \to X = Y))$
24	22 23	mpi	$⊢ 1 = 0 \to (Y = (X + 1) \mod N \to X = Y)$
25	24	imp	$⊢ (1 = 0 \land Y = (X + 1) \mod N) \to X = Y$
26	21 25	biimtrdi	$⊢ (X \in I \land Y \in I) \to (⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩ \to X = Y)$
27		1ex	$⊢ 1 \in V$
28	27	a1i	$⊢ Y \in I \to 1 \in V$
29	28	anim1i	$⊢ (Y \in I \land X \in I) \to (1 \in V \land X \in I)$
30	29	ancoms	$⊢ (X \in I \land Y \in I) \to (1 \in V \land X \in I)$
31		opthg2	$⊢ (1 \in V \land X \in I) \to (⟨1, Y⟩ = ⟨1, X⟩ \leftrightarrow (1 = 1 \land Y = X))$
32	30 31	syl	$⊢ (X \in I \land Y \in I) \to (⟨1, Y⟩ = ⟨1, X⟩ \leftrightarrow (1 = 1 \land Y = X))$
33		simpr	$⊢ (1 = 1 \land Y = X) \to Y = X$
34	33	eqcomd	$⊢ (1 = 1 \land Y = X) \to X = Y$
35	32 34	biimtrdi	$⊢ (X \in I \land Y \in I) \to (⟨1, Y⟩ = ⟨1, X⟩ \to X = Y)$
36		ovex	$⊢ (X - 1) \mod N \in V$
37	6 36	pm3.2i	$⊢ (0 \in V \land (X - 1) \mod N \in V)$
38		opthg2	$⊢ (0 \in V \land (X - 1) \mod N \in V) \to (⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩ \leftrightarrow (1 = 0 \land Y = (X - 1) \mod N))$
39	37 38	mp1i	$⊢ (X \in I \land Y \in I) \to (⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩ \leftrightarrow (1 = 0 \land Y = (X - 1) \mod N))$
40		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (Y = (X - 1) \mod N \to X = Y))$
41	22 40	mpi	$⊢ 1 = 0 \to (Y = (X - 1) \mod N \to X = Y)$
42	41	imp	$⊢ (1 = 0 \land Y = (X - 1) \mod N) \to X = Y$
43	39 42	biimtrdi	$⊢ (X \in I \land Y \in I) \to (⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩ \to X = Y)$
44	26 35 43	3jaod	$⊢ (X \in I \land Y \in I) \to ((⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, X⟩ \lor ⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y)$
45		op2ndg	$⊢ (0 \in V \land X \in I) \to 2^{nd} (⟨0, X⟩) = X$
46	9 45	syl	$⊢ (X \in I \land Y \in I) \to 2^{nd} (⟨0, X⟩) = X$
47		oveq1	$⊢ 2^{nd} (⟨0, X⟩) = X \to 2^{nd} (⟨0, X⟩) + 1 = X + 1$
48	47	oveq1d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (2^{nd} (⟨0, X⟩) + 1) \mod N = (X + 1) \mod N$
49	48	opeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ = ⟨0, (X + 1) \mod N⟩$
50	49	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \leftrightarrow ⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩)$
51		opeq2	$⊢ 2^{nd} (⟨0, X⟩) = X \to ⟨1, 2^{nd} (⟨0, X⟩)⟩ = ⟨1, X⟩$
52	51	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \leftrightarrow ⟨1, Y⟩ = ⟨1, X⟩)$
53		oveq1	$⊢ 2^{nd} (⟨0, X⟩) = X \to 2^{nd} (⟨0, X⟩) - 1 = X - 1$
54	53	oveq1d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (2^{nd} (⟨0, X⟩) - 1) \mod N = (X - 1) \mod N$
55	54	opeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩ = ⟨0, (X - 1) \mod N⟩$
56	55	eqeq2d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩ \leftrightarrow ⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩)$
57	50 52 56	3orbi123d	$⊢ 2^{nd} (⟨0, X⟩) = X \to ((⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \leftrightarrow (⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, X⟩ \lor ⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩))$
58	57	imbi1d	$⊢ 2^{nd} (⟨0, X⟩) = X \to (((⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y) \leftrightarrow ((⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, X⟩ \lor ⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y))$
59	46 58	syl	$⊢ (X \in I \land Y \in I) \to (((⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y) \leftrightarrow ((⟨1, Y⟩ = ⟨0, (X + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, X⟩ \lor ⟨1, Y⟩ = ⟨0, (X - 1) \mod N⟩) \to X = Y))$
60	44 59	mpbird	$⊢ (X \in I \land Y \in I) \to ((⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y)$
61	60	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \to ((⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) + 1) \mod N⟩ \lor ⟨1, Y⟩ = ⟨1, 2^{nd} (⟨0, X⟩)⟩ \lor ⟨1, Y⟩ = ⟨0, (2^{nd} (⟨0, X⟩) - 1) \mod N⟩) \to X = Y)$
62	17 61	syld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, X⟩, ⟨1, Y⟩\} \in E \to X = Y)$
63		simpr	$⊢ (X \in I \land Y \in I) \to Y \in I$
64	63	ad2antlr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \to Y \in I$
65		opeq2	$⊢ x = Y \to ⟨0, x⟩ = ⟨0, Y⟩$
66		oveq1	$⊢ x = Y \to x + 1 = Y + 1$
67	66	oveq1d	$⊢ x = Y \to (x + 1) \mod N = (Y + 1) \mod N$
68	67	opeq2d	$⊢ x = Y \to ⟨0, (x + 1) \mod N⟩ = ⟨0, (Y + 1) \mod N⟩$
69	65 68	preq12d	$⊢ x = Y \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} = \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\}$
70	69	eqeq2d	$⊢ x = Y \to (\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, Y⟩, ⟨0, (Y + 1) \mod N⟩\})$
71		opeq2	$⊢ x = Y \to ⟨1, x⟩ = ⟨1, Y⟩$
72	65 71	preq12d	$⊢ x = Y \to \{⟨0, x⟩, ⟨1, x⟩\} = \{⟨0, Y⟩, ⟨1, Y⟩\}$
73	72	eqeq2d	$⊢ x = Y \to (\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, Y⟩, ⟨1, Y⟩\})$
74		oveq1	$⊢ x = Y \to x + K = Y + K$
75	74	oveq1d	$⊢ x = Y \to (x + K) \mod N = (Y + K) \mod N$
76	75	opeq2d	$⊢ x = Y \to ⟨1, (x + K) \mod N⟩ = ⟨1, (Y + K) \mod N⟩$
77	71 76	preq12d	$⊢ x = Y \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} = \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\}$
78	77	eqeq2d	$⊢ x = Y \to (\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨1, Y⟩, ⟨1, (Y + K) \mod N⟩\})$
79	70 73 78	3orbi123d	$⊢ x = Y \to ((\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨1, x⟩, ⟨1, (x + 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⟩\}))$
80	79	adantl	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \land x = Y) \to ((\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨1, x⟩, ⟨1, (x + 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⟩\}))$
81		eqidd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \to \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, Y⟩, ⟨1, Y⟩\}$
82	81	3mix2d	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \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⟩\})$
83	64 80 82	rspcedvd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \to \exists x \in I (\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
84	2 1 3 4	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\{⟨0, Y⟩, ⟨1, Y⟩\} \in E \leftrightarrow \exists x \in I (\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
85	84	ad2antrr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \to (\{⟨0, Y⟩, ⟨1, Y⟩\} \in E \leftrightarrow \exists x \in I (\{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨0, x⟩, ⟨1, x⟩\} \lor \{⟨0, Y⟩, ⟨1, Y⟩\} = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
86	83 85	mpbird	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \to \{⟨0, Y⟩, ⟨1, Y⟩\} \in E$
87		opeq2	$⊢ X = Y \to ⟨0, X⟩ = ⟨0, Y⟩$
88	87	preq1d	$⊢ X = Y \to \{⟨0, X⟩, ⟨1, Y⟩\} = \{⟨0, Y⟩, ⟨1, Y⟩\}$
89	88	eleq1d	$⊢ X = Y \to (\{⟨0, X⟩, ⟨1, Y⟩\} \in E \leftrightarrow \{⟨0, Y⟩, ⟨1, Y⟩\} \in E)$
90	89	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \to (\{⟨0, X⟩, ⟨1, Y⟩\} \in E \leftrightarrow \{⟨0, Y⟩, ⟨1, Y⟩\} \in E)$
91	86 90	mpbird	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \land X = Y) \to \{⟨0, X⟩, ⟨1, Y⟩\} \in E$
92	91	ex	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \to (X = Y \to \{⟨0, X⟩, ⟨1, Y⟩\} \in E)$
93	62 92	impbid	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in I \land Y \in I)) \to (\{⟨0, X⟩, ⟨1, Y⟩\} \in E \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem gpgedgiov

Proof