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	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
	gpgprismgr4cycl.f	⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
	gpgprismgr4cycl.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
Assertion	gpgprismgr4cycl0	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) )

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
2		gpgprismgr4cycl.f	⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
3		gpgprismgr4cycl.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
4	1 2 3	gpgprismgr4cycllem11	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )
5	2	gpgprismgr4cycllem1	⊢ ( ♯ ‘ 𝐹 ) = 4
6	4 5	jctir	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) )