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=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
	gpgprismgr4cycl.g	No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
Assertion	gpgprismgr4cycl0	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(F\mathrm{Cycles}\left(G\right)P\wedge \left|F\right|=4\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	$$⊢P=⟨“⟨0,0⟩⟨0,1⟩⟨1,1⟩⟨1,0⟩⟨0,0⟩”⟩$$
2		gpgprismgr4cycl.f	$$⊢F=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
3		gpgprismgr4cycl.g	Could not format G = ( N gPetersenGr 1 ) : No typesetting found for |- G = ( N gPetersenGr 1 ) with typecode |-
4	1 2 3	gpgprismgr4cycllem11	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to F\mathrm{Cycles}\left(G\right)P$$
5	2	gpgprismgr4cycllem1	$$⊢\left|F\right|=4$$
6	4 5	jctir	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(F\mathrm{Cycles}\left(G\right)P\wedge \left|F\right|=4\right)$$