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 = ( 0 ..^ N )
	gpgprismgriedgdmel.g	|- G = ( N gPetersenGr 1 )
Assertion	gpgprismgriedgdmel	|- ( N e. ( ZZ>= ` 3 ) -> ( X e. dom ( iEdg ` G ) <-> E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )

Proof

Step	Hyp	Ref	Expression
1		gpgprismgriedgdmel.i	|- I = ( 0 ..^ N )
2		gpgprismgriedgdmel.g	|- G = ( N gPetersenGr 1 )
3		eluzge3nn	|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
4		1elfzo1ceilhalf1	|- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
5		eqid	|- ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
6	1 5 2	gpgiedgdmel	|- ( ( N e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( X e. dom ( iEdg ` G ) <-> E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
7	3 4 6	syl2anc	|- ( N e. ( ZZ>= ` 3 ) -> ( X e. dom ( iEdg ` G ) <-> E. x e. I ( X = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ X = { <. 0 , x >. , <. 1 , x >. } \/ X = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )