gpgedgel

Description: An edge in a generalized Petersen graph G . (Contributed by AV, 29-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		gpgvtxel.i	$⊢ I = (0 ..^N)$
2		gpgvtxel.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
3		gpgvtxel.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
4		gpgedgel.e	$⊢ E = Edg (G)$
5	3	fveq2i	Could not format ( Edg ` G ) = ( Edg ` ( N gPetersenGr K ) ) : No typesetting found for \|- ( Edg ` G ) = ( Edg ` ( N gPetersenGr K ) ) with typecode \|-
6	4 5	eqtri	Could not format E = ( Edg ` ( N gPetersenGr K ) ) : No typesetting found for \|- E = ( Edg ` ( N gPetersenGr K ) ) with typecode \|-
7	6	eleq2i	Could not format ( Y e. E <-> Y e. ( Edg ` ( N gPetersenGr K ) ) ) : No typesetting found for \|- ( Y e. E <-> Y e. ( Edg ` ( N gPetersenGr K ) ) ) with typecode \|-
8		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
9	2 1	gpgedg	Could not format ( ( N e. NN /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. I ) \| E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) : No typesetting found for \|- ( ( N e. NN /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. I ) \| E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) with typecode \|-
10	8 9	sylan	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. I ) \| E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Edg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. I ) \| E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) with typecode \|-
11	10	eleq2d	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Y e. ( Edg ` ( N gPetersenGr K ) ) <-> Y e. { e e. ~P ( { 0 , 1 } X. I ) \| E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Y e. ( Edg ` ( N gPetersenGr K ) ) <-> Y e. { e e. ~P ( { 0 , 1 } X. I ) \| E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) with typecode \|-
12	7 11	bitrid	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (Y \in E \leftrightarrow Y \in \{e \in 𝒫 (\{0, 1\} \times I) \| \exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})\})$
13		eqeq1	$⊢ e = Y \to (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\})$
14		eqeq1	$⊢ e = Y \to (e = \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow Y = \{⟨0, x⟩, ⟨1, x⟩\})$
15		eqeq1	$⊢ e = Y \to (e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
16	13 14 15	3orbi123d	$⊢ e = Y \to ((e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
17	16	rexbidv	$⊢ e = Y \to (\exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow \exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
18	17	elrab	$⊢ Y \in \{e \in 𝒫 (\{0, 1\} \times I) \| \exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})\} \leftrightarrow (Y \in 𝒫 (\{0, 1\} \times I) \land \exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
19		prex	$⊢ \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in V$
20	19	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in V$
21		c0ex	$⊢ 0 \in V$
22	21	prid1	$⊢ 0 \in \{0, 1\}$
23	22	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to 0 \in \{0, 1\}$
24		simpr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to x \in I$
25	23 24	opelxpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to ⟨0, x⟩ \in (\{0, 1\} \times I)$
26		elfzoelz	$⊢ x \in (0 ..^N) \to x \in ℤ$
27	26 1	eleq2s	$⊢ x \in I \to x \in ℤ$
28	27	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to x \in ℤ$
29	28	peano2zd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to x + 1 \in ℤ$
30	8	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℕ$
31	30	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to N \in ℕ$
32		zmodfzo	$⊢ (x + 1 \in ℤ \land N \in ℕ) \to (x + 1) \mod N \in (0 ..^N)$
33	29 31 32	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to (x + 1) \mod N \in (0 ..^N)$
34	33 1	eleqtrrdi	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to (x + 1) \mod N \in I$
35	23 34	opelxpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to ⟨0, (x + 1) \mod N⟩ \in (\{0, 1\} \times I)$
36	25 35	prssd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \subseteq \{0, 1\} \times I$
37	20 36	elpwd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I)$
38		eleq1	$⊢ Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \to (Y \in 𝒫 (\{0, 1\} \times I) \leftrightarrow \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I))$
39	37 38	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \to Y \in 𝒫 (\{0, 1\} \times I))$
40		prex	$⊢ \{⟨0, x⟩, ⟨1, x⟩\} \in V$
41	40	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \in V$
42		1ex	$⊢ 1 \in V$
43	42	prid2	$⊢ 1 \in \{0, 1\}$
44	43	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to 1 \in \{0, 1\}$
45	44 24	opelxpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to ⟨1, x⟩ \in (\{0, 1\} \times I)$
46	25 45	prssd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \subseteq \{0, 1\} \times I$
47	41 46	elpwd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \in 𝒫 (\{0, 1\} \times I)$
48		eleq1	$⊢ Y = \{⟨0, x⟩, ⟨1, x⟩\} \to (Y \in 𝒫 (\{0, 1\} \times I) \leftrightarrow \{⟨0, x⟩, ⟨1, x⟩\} \in 𝒫 (\{0, 1\} \times I))$
49	47 48	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to (Y = \{⟨0, x⟩, ⟨1, x⟩\} \to Y \in 𝒫 (\{0, 1\} \times I))$
50		prex	$⊢ \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in V$
51	50	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in V$
52		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
53	52 2	eleq2s	$⊢ K \in J \to K \in ℤ$
54	53	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \in ℤ$
55	54	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to K \in ℤ$
56	28 55	zaddcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to x + K \in ℤ$
57		zmodfzo	$⊢ (x + K \in ℤ \land N \in ℕ) \to (x + K) \mod N \in (0 ..^N)$
58	56 31 57	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to (x + K) \mod N \in (0 ..^N)$
59	58 1	eleqtrrdi	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to (x + K) \mod N \in I$
60	44 59	opelxpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to ⟨1, (x + K) \mod N⟩ \in (\{0, 1\} \times I)$
61	45 60	prssd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \subseteq \{0, 1\} \times I$
62	51 61	elpwd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I)$
63		eleq1	$⊢ Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \to (Y \in 𝒫 (\{0, 1\} \times I) \leftrightarrow \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I))$
64	62 63	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to (Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \to Y \in 𝒫 (\{0, 1\} \times I))$
65	39 49 64	3jaod	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land x \in I) \to ((Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \to Y \in 𝒫 (\{0, 1\} \times I))$
66	65	rexlimdva	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \to Y \in 𝒫 (\{0, 1\} \times I))$
67	66	pm4.71rd	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (Y \in 𝒫 (\{0, 1\} \times I) \land \exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})))$
68	18 67	bitr4id	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (Y \in \{e \in 𝒫 (\{0, 1\} \times I) \| \exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})\} \leftrightarrow \exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
69	12 68	bitrd	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (Y \in E \leftrightarrow \exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$

Metamath Proof Explorer

Theorem gpgedgel

Proof