Theorem pgjsgr

Description: A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025)

	Ref	Expression
Assertion	pgjsgr	Could not format assertion : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |-

Proof

Step	Hyp	Ref	Expression
1		5eluz3	$$⊢5\in {\mathbb{Z}}_{\ge 3}$$
2		pglem	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)$$
3		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 |-
4	1 2 3	mp2an	Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |-