Theorem gpgprismgrusgra

Description: The generalized Petersen graphs G(N,1), which are the N-prisms, are simple graphs. (Contributed by AV, 31-Oct-2025)

	Ref	Expression
Assertion	gpgprismgrusgra	Could not format assertion : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1zzd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \mathbb{Z}$$
2		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in ℝ$$
3		2re	$$⊢2\in ℝ$$
4	3	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\in ℝ$$
5		2ne0	$$⊢2\ne 0$$
6	5	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\ne 0$$
7	2 4 6	3jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(N\in ℝ\wedge 2\in ℝ\wedge 2\ne 0\right)$$
8		redivcl	$$⊢\left(N\in ℝ\wedge 2\in ℝ\wedge 2\ne 0\right)\to \frac{N}{2}\in ℝ$$
9	7 8	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \frac{N}{2}\in ℝ$$
10	9	ceilcld	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⌈\frac{N}{2}⌉\in \mathbb{Z}$$
11		1red	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in ℝ$$
12	8	ceilcld	$$⊢\left(N\in ℝ\wedge 2\in ℝ\wedge 2\ne 0\right)\to ⌈\frac{N}{2}⌉\in \mathbb{Z}$$
13	7 12	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⌈\frac{N}{2}⌉\in \mathbb{Z}$$
14	13	zred	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⌈\frac{N}{2}⌉\in ℝ$$
15		1lt2	$$⊢1<2$$
16	15	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<2$$
17		2ltceilhalf	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\le ⌈\frac{N}{2}⌉$$
18	11 4 14 16 17	ltletrd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<⌈\frac{N}{2}⌉$$
19		fzolb	$$⊢1\in \left(1..^⌈\frac{N}{2}⌉\right)\leftrightarrow \left(1\in \mathbb{Z}\wedge ⌈\frac{N}{2}⌉\in \mathbb{Z}\wedge 1<⌈\frac{N}{2}⌉\right)$$
20	1 10 18 19	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{N}{2}⌉\right)$$
21		gpgusgra	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr 1 ) e. USGraph ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr 1 ) e. USGraph ) with typecode |-
22	20 21	mpdan	Could not format ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph ) with typecode |-