Theorem gpg5order

Description: The order of a generalized Petersen graph G(5,K), which is either the Petersen graph G(5,2) or the 5-prism G(5,1), is 10. (Contributed by AV, 26-Aug-2025)

	Ref	Expression
Assertion	gpg5order	⊢ ( 𝐾 ∈ ( 1 ... 2 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 𝐾 ) ) ) = ; 1 0 )

Proof

Step	Hyp	Ref	Expression
1		5nn	⊢ 5 ∈ ℕ
2		2z	⊢ 2 ∈ ℤ
3		fzval3	⊢ ( 2 ∈ ℤ → ( 1 ... 2 ) = ( 1 ..^ ( 2 + 1 ) ) )
4	2 3	ax-mp	⊢ ( 1 ... 2 ) = ( 1 ..^ ( 2 + 1 ) )
5		2p1e3	⊢ ( 2 + 1 ) = 3
6		ceil5half3	⊢ ( ⌈ ‘ ( 5 / 2 ) ) = 3
7	5 6	eqtr4i	⊢ ( 2 + 1 ) = ( ⌈ ‘ ( 5 / 2 ) )
8	7	oveq2i	⊢ ( 1 ..^ ( 2 + 1 ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
9	4 8	eqtri	⊢ ( 1 ... 2 ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
10	9	eleq2i	⊢ ( 𝐾 ∈ ( 1 ... 2 ) ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
11	10	biimpi	⊢ ( 𝐾 ∈ ( 1 ... 2 ) → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
12		eqid	⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
13	12	gpgorder	⊢ ( ( 5 ∈ ℕ ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 𝐾 ) ) ) = ( 2 · 5 ) )
14	1 11 13	sylancr	⊢ ( 𝐾 ∈ ( 1 ... 2 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 𝐾 ) ) ) = ( 2 · 5 ) )
15		5cn	⊢ 5 ∈ ℂ
16		2cn	⊢ 2 ∈ ℂ
17		5t2e10	⊢ ( 5 · 2 ) = ; 1 0
18	15 16 17	mulcomli	⊢ ( 2 · 5 ) = ; 1 0
19	14 18	eqtrdi	⊢ ( 𝐾 ∈ ( 1 ... 2 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 𝐾 ) ) ) = ; 1 0 )