Metamath Proof Explorer


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
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 K 1 2 K 1 ..^ 5 2
11 10 biimpi K 1 2 K 1 ..^ 5 2
12 eqid 1 ..^ 5 2 = 1 ..^ 5 2
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
16 2cn 2
17 5t2e10 5 2 = 10
18 15 16 17 mulcomli 2 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 |-