Theorem gpgprismgriedgdmel

Description: An index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Hypotheses	gpgprismgriedgdmel.i	$$⊢I=\left(0..^N\right)$$
	gpgprismgriedgdmel.g	No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
Assertion	gpgprismgriedgdmel	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(X\in \mathrm{dom}\mathrm{iEdg}\left(G\right)\leftrightarrow \exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgriedgdmel.i	$$⊢I=\left(0..^N\right)$$
2		gpgprismgriedgdmel.g	Could not format G = ( N gPetersenGr 1 ) : No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
3		eluzge3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
4		1elfzo1ceilhalf1	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{N}{2}⌉\right)$$
5		eqid	$$⊢\left(1..^⌈\frac{N}{2}⌉\right)=\left(1..^⌈\frac{N}{2}⌉\right)$$
6	1 5 2	gpgiedgdmel	$$⊢\left(N\in \mathbb{N}\wedge 1\in \left(1..^⌈\frac{N}{2}⌉\right)\right)\to \left(X\in \mathrm{dom}\mathrm{iEdg}\left(G\right)\leftrightarrow \exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
7	3 4 6	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(X\in \mathrm{dom}\mathrm{iEdg}\left(G\right)\leftrightarrow \exists x\in I\left(X=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee X=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee X=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$