Metamath Proof Explorer

Theorem gpg5ngric

Description: The two generalized Petersen graphs G(5,K) of order 10, which are the Petersen graph G(5,2) and the 5-prism G(5,1), are not isomorphic. (Contributed by AV, 22-Nov-2025)

Ref Expression
Assertion gpg5ngric 
|- -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 )

Proof

Step Hyp Ref Expression
1 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
2 1elfzo1ceilhalf1 
 |-  ( 5 e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
3 1 2 ax-mp 
 |-  1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
4 1 3 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
5 gpgusgra 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph )
6 usgruspgr 
 |-  ( ( 5 gPetersenGr 1 ) e. USGraph -> ( 5 gPetersenGr 1 ) e. USPGraph )
7 4 5 6 mp2b 
 |-  ( 5 gPetersenGr 1 ) e. USPGraph
8 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
9 1 8 pm3.2i 
 |-  ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
10 gpgusgra 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph )
11 usgruspgr 
 |-  ( ( 5 gPetersenGr 2 ) e. USGraph -> ( 5 gPetersenGr 2 ) e. USPGraph )
12 9 10 11 mp2b 
 |-  ( 5 gPetersenGr 2 ) e. USPGraph
13 7 12 pm3.2i 
 |-  ( ( 5 gPetersenGr 1 ) e. USPGraph /\ ( 5 gPetersenGr 2 ) e. USPGraph )
14 gpgprismgr4cyclex 
 |-  ( 5 e. ( ZZ>= ` 3 ) -> E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) )
15 1 14 ax-mp 
 |-  E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 )
16 pg4cyclnex 
 |-  -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 )
17 15 16 pm3.2i 
 |-  ( E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) /\ -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) )
18 cycldlenngric 
 |-  ( ( ( 5 gPetersenGr 1 ) e. USPGraph /\ ( 5 gPetersenGr 2 ) e. USPGraph ) -> ( ( E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) /\ -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) ) -> -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) ) )
19 13 17 18 mp2 
 |-  -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 )