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	⊢ 𝐼 = ( 0 ..^ 𝑁 )
	gpgprismgriedgdmel.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
Assertion	gpgprismgriedgdmel	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑋 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑋 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑋 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		gpgprismgriedgdmel.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		gpgprismgriedgdmel.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
3		eluzge3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
4		1elfzo1ceilhalf1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
5		eqid	⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
6	1 5 2	gpgiedgdmel	⊢ ( ( 𝑁 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑋 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑋 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑋 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) )
7	3 4 6	syl2anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑋 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑋 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑋 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) ) )