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	Could not format assertion : No typesetting found for |- ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ; 1 0 ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		5nn	$$⊢5\in \mathbb{N}$$
2		2z	$$⊢2\in \mathbb{Z}$$
3		fzval3	$$⊢2\in \mathbb{Z}\to \left(1\dots 2\right)=\left(1..^2+1\right)$$
4	2 3	ax-mp	$$⊢\left(1\dots 2\right)=\left(1..^2+1\right)$$
5		2p1e3	$$⊢2+1=3$$
6		ceil5half3	$$⊢⌈\frac{5}{2}⌉=3$$
7	5 6	eqtr4i	$$⊢2+1=⌈\frac{5}{2}⌉$$
8	7	oveq2i	$$⊢\left(1..^2+1\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
9	4 8	eqtri	$$⊢\left(1\dots 2\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
10	9	eleq2i	$$⊢K\in \left(1\dots 2\right)\leftrightarrow K\in \left(1..^⌈\frac{5}{2}⌉\right)$$
11	10	biimpi	$$⊢K\in \left(1\dots 2\right)\to K\in \left(1..^⌈\frac{5}{2}⌉\right)$$
12		eqid	$$⊢\left(1..^⌈\frac{5}{2}⌉\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
13	12	gpgorder	Could not format ( ( 5 e. NN /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ( 2 x. 5 ) ) : No typesetting found for |- ( ( 5 e. NN /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ( 2 x. 5 ) ) with typecode |-
14	1 11 13	sylancr	Could not format ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ( 2 x. 5 ) ) : No typesetting found for |- ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ( 2 x. 5 ) ) with typecode |-
15		5cn	$$⊢5\in ℂ$$
16		2cn	$$⊢2\in ℂ$$
17		5t2e10	$$⊢5\cdot 2=10$$
18	15 16 17	mulcomli	$$⊢2\cdot 5=10$$
19	14 18	eqtrdi	Could not format ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ; 1 0 ) : No typesetting found for |- ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ; 1 0 ) with typecode |-