Theorem gpgprismgr4cycl0

Description: The generalized Petersen graphs G(N,1), which are the N-prisms, have a cycle of length 4 starting at the vertex <. 0 , 0 >. . (Contributed by AV, 5-Nov-2025)

	Ref	Expression
Hypotheses	gpgprismgr4cycl.p	|- P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
	gpgprismgr4cycl.f	|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
	gpgprismgr4cycl.g	|- G = ( N gPetersenGr 1 )
Assertion	gpgprismgr4cycl0	|- ( N e. ( ZZ>= ` 3 ) -> ( F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) )

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	|- P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
2		gpgprismgr4cycl.f	|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
3		gpgprismgr4cycl.g	|- G = ( N gPetersenGr 1 )
4	1 2 3	gpgprismgr4cycllem11	|- ( N e. ( ZZ>= ` 3 ) -> F ( Cycles ` G ) P )
5	2	gpgprismgr4cycllem1	|- ( # ` F ) = 4
6	4 5	jctir	|- ( N e. ( ZZ>= ` 3 ) -> ( F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) )