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	|- ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ; 1 0 )

Proof

Step	Hyp	Ref	Expression
1		5nn	|- 5 e. NN
2		2z	|- 2 e. ZZ
3		fzval3	|- ( 2 e. ZZ -> ( 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	|- ( K e. ( 1 ... 2 ) <-> K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
11	10	biimpi	|- ( K e. ( 1 ... 2 ) -> K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
12		eqid	|- ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
13	12	gpgorder	|- ( ( 5 e. NN /\ K e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ( 2 x. 5 ) )
14	1 11 13	sylancr	|- ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ( 2 x. 5 ) )
15		5cn	|- 5 e. CC
16		2cn	|- 2 e. CC
17		5t2e10	|- ( 5 x. 2 ) = ; 1 0
18	15 16 17	mulcomli	|- ( 2 x. 5 ) = ; 1 0
19	14 18	eqtrdi	|- ( K e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ; 1 0 )