Metamath Proof Explorer

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 
|- ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph )

Proof

Step Hyp Ref Expression
1 1zzd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ZZ )
2 eluzelre 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. RR )
5 2ne0 
 |-  2 =/= 0
6 5 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 =/= 0 )
7 2 4 6 3jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N e. RR /\ 2 e. RR /\ 2 =/= 0 ) )
8 redivcl 
 |-  ( ( N e. RR /\ 2 e. RR /\ 2 =/= 0 ) -> ( N / 2 ) e. RR )
9 7 8 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N / 2 ) e. RR )
10 9 ceilcld 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
11 1red 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. RR )
12 8 ceilcld 
 |-  ( ( N e. RR /\ 2 e. RR /\ 2 =/= 0 ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
13 7 12 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
14 13 zred 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. RR )
15 1lt2 
 |-  1 < 2
16 15 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 < 2 )
17 2ltceilhalf 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 <_ ( |^ ` ( N / 2 ) ) )
18 11 4 14 16 17 ltletrd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 < ( |^ ` ( N / 2 ) ) )
19 fzolb 
 |-  ( 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( 1 e. ZZ /\ ( |^ ` ( N / 2 ) ) e. ZZ /\ 1 < ( |^ ` ( N / 2 ) ) ) )
20 1 10 18 19 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
21 gpgusgra 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr 1 ) e. USGraph )
22 20 21 mpdan 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph )