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	Could not format assertion : No typesetting found for |- -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		5eluz3	$$⊢5\in {\mathbb{Z}}_{\ge 3}$$
2		1elfzo1ceilhalf1	$$⊢5\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{5}{2}⌉\right)$$
3	1 2	ax-mp	$$⊢1\in \left(1..^⌈\frac{5}{2}⌉\right)$$
4	1 3	pm3.2i	$$⊢\left(5\in {\mathbb{Z}}_{\ge 3}\wedge 1\in \left(1..^⌈\frac{5}{2}⌉\right)\right)$$
5		gpgusgra	Could not format ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph ) : No typesetting found for |- ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph ) with typecode |-
6		usgruspgr	Could not format ( ( 5 gPetersenGr 1 ) e. USGraph -> ( 5 gPetersenGr 1 ) e. USPGraph ) : No typesetting found for |- ( ( 5 gPetersenGr 1 ) e. USGraph -> ( 5 gPetersenGr 1 ) e. USPGraph ) with typecode |-
7	4 5 6	mp2b	Could not format ( 5 gPetersenGr 1 ) e. USPGraph : No typesetting found for |- ( 5 gPetersenGr 1 ) e. USPGraph with typecode |-
8		pglem	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)$$
9	1 8	pm3.2i	$$⊢\left(5\in {\mathbb{Z}}_{\ge 3}\wedge 2\in \left(1..^⌈\frac{5}{2}⌉\right)\right)$$
10		gpgusgra	Could not format ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph ) : No typesetting found for |- ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph ) with typecode |-
11		usgruspgr	Could not format ( ( 5 gPetersenGr 2 ) e. USGraph -> ( 5 gPetersenGr 2 ) e. USPGraph ) : No typesetting found for |- ( ( 5 gPetersenGr 2 ) e. USGraph -> ( 5 gPetersenGr 2 ) e. USPGraph ) with typecode |-
12	9 10 11	mp2b	Could not format ( 5 gPetersenGr 2 ) e. USPGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USPGraph with typecode |-
13	7 12	pm3.2i	Could not format ( ( 5 gPetersenGr 1 ) e. USPGraph /\ ( 5 gPetersenGr 2 ) e. USPGraph ) : No typesetting found for |- ( ( 5 gPetersenGr 1 ) e. USPGraph /\ ( 5 gPetersenGr 2 ) e. USPGraph ) with typecode |-
14		gpgprismgr4cyclex	Could not format ( 5 e. ( ZZ>= ` 3 ) -> E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) ) : No typesetting found for |- ( 5 e. ( ZZ>= ` 3 ) -> E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) ) with typecode |-
15	1 14	ax-mp	Could not format E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) : No typesetting found for |- E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) with typecode |-
16		pg4cyclnex	Could not format -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) : No typesetting found for |- -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) with typecode |-
17	15 16	pm3.2i	Could not format ( E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) /\ -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) ) : No typesetting found for |- ( E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 1 ) ) p /\ ( # ` f ) = 4 ) /\ -. E. p E. f ( f ( Cycles ` ( 5 gPetersenGr 2 ) ) p /\ ( # ` f ) = 4 ) ) with typecode |-
18		cycldlenngric	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
19	13 17 18	mp2	Could not format -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) : No typesetting found for |- -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) with typecode |-